Proposition 3 and the limit of Γ_T in Proposition S5

This file assembles Proposition 3 of the paper and the limit of Γ_T/log log T of Proposition S5 of the supplementary material from the bounds of RateUpper.lean, RateLower.lean, and RateMixture.lean, and from the lower bound (S9) of Lemma S6 (lem_fixedk_proof). The limit of log η_T/log log T of Proposition S5 is in RateEveryRho.lean.

• fixedKBound_le_of_lem_fixedk: the conclusion of Lemma S6 in the form fixedKBound ≤ Γ_T;
• prop_mixture_of_fixedK: Proposition 3, following its proof in Section S1.6: the lower bound of (i) from (S9), the upper bound from Γ_T ≤ log η_T (Proposition 1(iii)) and Lemma S3, and (ii) from RateMixture.lean;
• isNumeraire_gaussNumeraire_mixAlt_of_div_le: for t ≥ 1 with (1 − s²)/t ≤ ρ², the proof of Proposition 2 applies at the horizon t, and ∏_{i=2}^t ℓ(Y_i) is the numéraire of Q at t;
• regret_gaussNumeraire_div: for any numéraires Es of Q and b ∈ [1, ∞), the regret of Π_t/b, with Π_t = ∏_{i=2}^t ℓ(Y_i), is log b + d_t, where d_t = E_Q(log Es_t) − (t − 1)κ is the difference ν_t − E_Q(log Π_t) of the proof of Proposition S5 (Lemma S1);
• exists_minimaxRegret_le_log_eta_add: Γ_T ≤ C + log η'_T for T ≥ 1, where η'_T is the value of Lemma 2(ii) and C = max_{t < t_ρ} d_t;
• tendsto_minimaxRegret_of_fixedK: Γ_T/log log T → 1 − s² for any numéraires of Q and every ρ > 0, the first limit of Proposition S5;
• prop_mixture_proof: Proposition 3.

In the proof of Proposition S5, the paper bounds d_t by C = max_{t < t_ρ} d_t; we take the sum of the |d_t| over t < t_ρ, which is also a bound. The integer t_ρ is here ⌈(1 − s²)/ρ²⌉ + 1, at least the paper's ⌈(1 − s²)/ρ²⌉, so that t_ρ ≥ 1.

Lemma S6 in the form of RateLower.lean

theorem LogOptimal.fixedKBound_le_of_lem_fixedk {s ρ : ℝ} {Γ : ℕ → EReal} (h : ∀ (r K T : ℕ) (c : ℝ), 4 ≤ r → 1 ≤ K → r ^ K ≤ T → 0 < c → have γ := √(ρ ^ 2 + s ^ 2); have β := lbBeta s ρ K c; have β' := lbBetaPrime s ρ; have c' := lbCPrime r c; 0 < c' → β' ≤ β → ↑(β - (β - β') * ↑K * Real.exp (-c' ^ 2 / (2 * s ^ 2)) - (2 * (c + 1) / γ + 2 * (c + 1) ^ 2 / (3 * γ ^ 2)) / (↑K + 1)) ≤ Γ T) (r K T : ℕ) (c : ℝ) : 4 ≤ r → 1 ≤ K → r ^ K ≤ T → 0 < c → 0 < lbCPrime r c → lbBetaPrime s ρ ≤ lbBeta s ρ K c → ↑(fixedKBound s ρ r K c) ≤ Γ T

The conclusion of Lemma S6, with its let bindings, in the form fixedKBound ≤ Γ_T.

Proposition 3

theorem LogOptimal.prop_mixture_of_fixedK {s ρ : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hρ0 : 0 ≤ ρ) (hρ : 1 - s ^ 2 ≤ ρ ^ 2) (hS9 : ∀ (r K T : ℕ) (c : ℝ), 4 ≤ r → 1 ≤ K → r ^ K ≤ T → 0 < c → 0 < lbCPrime r c → lbBetaPrime s ρ ≤ lbBeta s ρ K c → ↑(fixedKBound s ρ r K c) ≤ minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T) : (Filter.Tendsto (fun (T : ℕ) => minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2)) ∧ Filter.Tendsto (fun (T : ℕ) => (eta gaussNull (gaussNumeraire s) T).log / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2))) ∧ IsEProcess gaussNull (mixtureEProcess s) ∧ Filter.limsup (fun (t : ℕ) => regret (mixAlt s ρ) (gaussNumeraire s t) (mixtureEProcess s t) / ↑(Real.log (Real.log ↑t))) Filter.atTop = ↑(1 - s ^ 2)

Proposition 3, given the lower bound (S9) of Lemma S6 for the numéraires of Proposition 2.

The numéraire at the horizons t ≥ t_ρ

theorem LogOptimal.isNumeraire_gaussNumeraire_mixAlt_of_div_le {s ρ : ℝ} (hs : 0 < s) {t : ℕ} (ht : 1 ≤ t) (hv : (1 - s ^ 2) / ↑t ≤ ρ ^ 2) : IsNumeraire gaussNull (mixAlt s ρ) t (gaussNumeraire s t)

For t ≥ 1 with (1 − s²)/t ≤ ρ², the mixing variance ρ² − (1 − s²)/t is nonnegative, and the proof of Proposition 2 shows that E*_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire of Q at the horizon t, with P*_t = ∫ P_{θ,t} N{0, ρ² − (1 − s²)/t}(dθ).

The upper bound of Proposition S5

theorem LogOptimal.regret_gaussNumeraire_div {s ρ : ℝ} (hs : 0 < s) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hS : Setting gaussNull (mixAlt s ρ) Es) (t : ℕ) {b : ENNReal} (hb1 : 1 ≤ b) (hb : b ≠ ⊤) : (regret (mixAlt s ρ) (Es t) fun (x : ℕ → ℝ) => gaussNumeraire s t x / b) = ↑(Real.log b.toReal + (∫ (x : ℕ → ℝ), (Es t x).log.toReal ∂mixAlt s ρ - ↑(t - 1) * kappa s))

The regret of Π_t/b (proof of Proposition S5): for any numéraires Es of Q, every t, and b ∈ [1, ∞), the regret of Π_t/b with Π_t = ∏_{i=2}^t ℓ(Y_i) is log b + d_t, where d_t = E_Q(log Es_t) − (t − 1)κ, by Lemma S1 and E_Q(log Π_t) = (t − 1)κ.

theorem LogOptimal.exists_minimaxRegret_le_log_eta_add {s ρ : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hEs : ∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) : ∃ (C : ℝ), ∀ (T : ℕ), 1 ≤ T → minimaxRegret gaussNull (mixAlt s ρ) Es T ≤ (eta gaussNull (gaussNumeraire s) T).log + ↑C

The upper bound of Proposition S5: for every ρ > 0 and any numéraires Es of Q, there is a constant C with Γ_T ≤ log η_T + C for T ≥ 1, where η_T is the value of the stopping problem of Lemma 2(ii). The process (Π_{t∧T}/η_T)_{t≥0} is an e-process, and its regret at t ≤ T is log η_T + d_t, where d_t = 0 for t ≥ t_ρ, since Π_t is then the numéraire. The e-process property does not involve the alternative; we take it from Proposition 1(iii) for the mixture with ρ = 1, whose numéraires are the Π_t (Proposition 2).

Proposition S5

theorem LogOptimal.tendsto_minimaxRegret_of_fixedK {s ρ : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hEs : ∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) (hS9 : ∀ (r K T : ℕ) (c : ℝ), 4 ≤ r → 1 ≤ K → r ^ K ≤ T → 0 < c → 0 < lbCPrime r c → lbBetaPrime s ρ ≤ lbBeta s ρ K c → ↑(fixedKBound s ρ r K c) ≤ minimaxRegret gaussNull (mixAlt s ρ) Es T) : Filter.Tendsto (fun (T : ℕ) => minimaxRegret gaussNull (mixAlt s ρ) Es T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2))

Proposition S5, the limit: for every ρ > 0 and any numéraires Es of Q, given the lower bound (S9) of Lemma S6, Γ_T/log log T → 1 − s².

Proposition 3 from Lemma S6

theorem LogOptimal.prop_mixture_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → (Filter.Tendsto (fun (T : ℕ) => minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2)) ∧ Filter.Tendsto (fun (T : ℕ) => (eta gaussNull (gaussNumeraire s) T).log / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2))) ∧ IsEProcess gaussNull (mixtureEProcess s) ∧ Filter.limsup (fun (t : ℕ) => regret (mixAlt s ρ) (gaussNumeraire s t) (mixtureEProcess s t) / ↑(Real.log (Real.log ↑t))) Filter.atTop = ↑(1 - s ^ 2)

Proposition 3.