Lemmas S4 and S6

This file completes the proofs of Lemmas S4 and S6 of the supplementary material from the intermediate theorems lem_lbmix_of_duality and lem_fixedk_of_duality, with the setting of Sections 1 and 2 for the mixture Q and every ρ > 0 (setting_mixAlt_of_isNumeraire) and Lemma 1 (lem_duality_proof).

• lem_lbmix_proof: Lemma S4;
• lem_fixedk_proof: Lemma S6.

theorem LogOptimal.lem_lbmix_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 < ρ → ∀ (Es : ℕ → (ℕ → ℝ) → ENNReal), (∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) → ∀ (r K T : ℕ) (c : ℝ), 4 ≤ r → 1 ≤ K → r ^ K ≤ T → 0 < c → lbMixture s ρ r K c ∈ stoppedMixtures gaussNull ∧ (↑(↑K + 1)⁻¹ * ∑ k ∈ Finset.range (K + 1), eIntegral (mixAlt s ρ) fun (x : ℕ → ℝ) => (ENNReal.ofReal ((↑K + 1) * lbJ s ρ r K c k x)).log) ≤ minimaxRegret gaussNull (mixAlt s ρ) Es T

theorem LogOptimal.lem_fixedk_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 < ρ → ∀ (Es : ℕ → (ℕ → ℝ) → ENNReal), (∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) → ∀ (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)) ≤ minimaxRegret gaussNull (mixAlt s ρ) Es T