Proposition S1(ii): exactness of Lemma 1 and the minimax identity #
This file proves Proposition S1 of the paper. Part (i) is Setting.exists_isEProcess_versions of
Duality/Finite.lean. Part (ii), the identity Γ_T = max_{ξ∈Δ_T} inf_{(E_t)} ∑_t ξ_t R_t(E_t) on
every sample space, follows from Sion's minimax theorem (Mathlib's Sion.minimax'). Part (iii),
eq. (S11), follows from the primal-dual equivalence of Koolen and Grünwald (2022, Theorem 5), the
hypothesis KoolenGrunwaldTheorem5, and from Lemma 1.
convex_probVectors,isCompact_probVectors:Δ_Tis convex and compact;regretSet 𝔓 Q Es T: the set of the vectorsv ∈ ℝ^{T+1}withR_t(E_t) ≤ v_tfor allt ≤ Tand some e-process(E_t); it is convex (Setting.convex_regretSet), since the regret is convex in the e-variable (Setting.regret_combination_le);Setting.minimaxRegret_eq_iInf_regretSet:Γ_T = inf_{v} max_t v_tover this set;Setting.iInf_sum_mul_regret_eq:inf_{(E_t)} ∑_t ξ_t R_t(E_t) = inf_v ∑_t ξ_t v_t, by the processes(1 − ε)E_t + εof the paper, whose regrets are finite and exceed those of(E_t)by at mostlog{1/(1 − ε)};Setting.iSup_iInf_eq_minimaxRegret: Sion's theorem with the compact convex setΔ_T;Setting.exists_minimax: the supremum overξis attained, sinceξ ↦ inf_v ∑_t ξ_t v_tis upper semicontinuous on the compact setΔ_T;prop_minimax_proof: Proposition S1.
As in the paper, Sion's theorem is applied to the bilinear function (ξ, v) ↦ ∑_t ξ_t v_t on Δ_T
and the convex set of the vectors that dominate the regrets of some e-process, which needs no
topology on e-processes, and the processes (1 − ε)E_t + ε relate the two infima. Before the
formalization, the paper applied Sion's theorem to e-processes and stated part (ii) for a finite
𝒳 only (its Section S5).
The simplex Δ_T #
The simplex Δ_T is convex.
The simplex Δ_T is compact, as a closed subset of [0, 1]^{T+1}.
Arithmetic in [−∞, ∞] #
The convex set of dominated regret vectors #
The constant process E_t = 1 is an e-process.
The set of the vectors v ∈ ℝ^{T+1} with R_t(E_t) ≤ v_t for all t ≤ T, for some
e-process (E_t).
Equations
Instances For
For E ∈ ℰ_t with a finite regret, log E is Q-integrable and finite Q-almost surely, and
E_Q(log E) is the integral of its real part.
The regret is convex in the e-variable: for a, b ≥ 0 with a + b = 1,
R_t(aE + bF) ≤ a R_t(E) + b R_t(F), by the concavity of the logarithm.
The set regretSet 𝔓 Q Es T is convex, since a convex combination of two e-processes stopped at
T is an e-process and the regret is convex.
Γ_T = inf_v max_t v_t over the vectors that dominate the regrets of some e-process.
For an e-process (E_t) and δ > 0, the process (1 − ε)E_{t∧T} + ε with
log{1/(1 − ε)} = δ has finite regrets, at most δ + R_t(E_t) for t ≤ T.
inf_{(E_t)} ∑_t ξ_t R_t(E_t) = inf_v ∑_t ξ_t v_t over the vectors that dominate the regrets of
some e-process.
Sion's minimax theorem with the compact convex set Δ_T, applied to (ξ, v) ↦ ∑_t ξ_t v_t
on Δ_T and the convex set of the vectors that dominate the regrets of some e-process:
sup_ξ inf_v ∑_t ξ_t v_t = inf_v max_t v_t = Γ_T.
The minimax identity of Proposition S1(ii): some ξ ∈ Δ_T attains
Γ_T = max_{ξ∈Δ_T} inf_{(E_t)} ∑_t ξ_t R_t(E_t). The function ξ ↦ inf_v ∑_t ξ_t v_t is upper
semicontinuous on the compact set Δ_T, as an infimum of continuous functions.