Proposition 4: the case s ≥ 1

This file proves Proposition 4 of the paper, following its proof in Section S1.8, and the claim of Section 4.3 that the minimax regret is also bounded in the worst case over μ for s ≥ 1.

• prop_sge1_proof: Proposition 4. By Proposition 1(iii) and Lemma 2(ii), Γ_T ≤ log η_T ≤ log s, since h_t ≤ s for s ≥ 1; the limit log η_T → log s follows from the limit η_T → s (tendsto_walkValue, under the law of the iterated logarithm) and the continuity of the logarithm on [0, ∞].
• regret_congr_numeraire: the regret does not depend on the version of the numéraire.
• sec4_sge1_worst_case_proof: for s ≥ 1, E*_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire of every Q_μ (Proposition S4), so that the e-process (E*_{t∧T}/η_T)_{t≥0} of Proposition 1(iii) has regret log η_T ≤ log s against every Q_μ at every t ≤ T.

theorem LogOptimal.prop_sge1_proof (s ρ : ℝ) : 1 ≤ s → 0 ≤ ρ → (∀ (T : ℕ), minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T ≤ (eta gaussNull (gaussNumeraire s) T).log ∧ (eta gaussNull (gaussNumeraire s) T).log ≤ ↑(Real.log s)) ∧ (LawOfIteratedLogarithm → Filter.Tendsto (fun (T : ℕ) => (eta gaussNull (gaussNumeraire s) T).log) Filter.atTop (nhds ↑(Real.log s)))

theorem LogOptimal.regret_congr_numeraire {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Q : MeasureTheory.Measure Ω} {Es Es' E : Ω → ENNReal} (h : Es =ᵐ[Q] Es') : regret Q Es E = regret Q Es' E

The regret does not depend on the version of the numéraire: two numéraires equal Q-almost surely give the same regrets.

theorem LogOptimal.sec4_sge1_worst_case_proof (s : ℝ) : 1 ≤ s → ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → ∀ (T : ℕ), (∀ t ≤ T, (⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) fun (x : ℕ → ℝ) => gaussNumeraire s (min t T) x / eta gaussNull (gaussNumeraire s) T) ≤ ↑(Real.log s)) ∧ worstCaseMinimaxRegret s Esμ T ≤ ↑(Real.log s)