Proposition S5 and Proposition 3(i) for every ρ > 0

This file proves the limit of log η_T/log log T in Proposition S5, for any numéraires Es of Q, following its proof in Section S2.5: Γ_T ≤ log η_T (Proposition 1(iii)), and η_T ≤ t_ρ + η'_T, where η'_T is the value of the stopping problem of Lemma 2(ii). Indeed, for t ≥ t_ρ, the numéraire Es_t equals Π_t = ∏_{i=2}^t ℓ(Y_i) Q-almost surely, hence P_θ-almost surely, and for t < t_ρ, E_θ(Es_t) ≤ 1. Section 4.3 of the paper cites Proposition S5 for the claim that Proposition 3(i) holds for every ρ > 0.

• marginal_nullDist_absolutelyContinuous: P_{θ,t} ≪ Q_t for t ≥ 1, since the distributions of (X̄_t, Y^t) are N(θ, 1/t) ⊗ N(0, 1)^{⊗(t−1)} and ∫ N(m, s²/t) N(0, ρ²)(dm) ⊗ N(0, s²)^{⊗(t−1)}, and the map x^t ↦ (x̄_t, Y^t) is a measurable embedding;
• ae_eq_nullDist_of_ae_eq_mixAlt: two ℱ_t-measurable functions equal Q-almost surely are equal P_θ-almost surely;
• eta_le_add_eta_gaussNumeraire: η_T ≤ t_ρ + η'_T;
• sec4_every_rho_proof: the claim of Section 4.3;
• prop_smallrho_proof: Proposition S5.

P_{θ,t} ≪ Q_t

theorem LogOptimal.marginal_nullDist_absolutelyContinuous {s : ℝ} (hs : 0 < s) (ρ θ : ℝ) {t : ℕ} (ht : 1 ≤ t) : (marginal (nullDist θ) t).AbsolutelyContinuous (marginal (mixAlt s ρ) t)

P_{θ,t} ≪ Q_t for t ≥ 1.

theorem LogOptimal.ae_eq_nullDist_of_ae_eq_mixAlt {s : ℝ} (hs : 0 < s) (ρ θ : ℝ) {t : ℕ} (ht : 1 ≤ t) {f g : (ℕ → ℝ) → ENNReal} (hf : Measurable f) (hg : Measurable g) (h : f =ᵐ[mixAlt s ρ] g) : f =ᵐ[nullDist θ] g

Two ℱ_t-measurable functions equal Q-almost surely are equal P_θ-almost surely, for t ≥ 1.

η_T ≤ t_ρ + η'_T

theorem LogOptimal.eta_le_add_eta_gaussNumeraire {s ρ : ℝ} (hs0 : 0 < s) (hρ : 0 < ρ) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hEs : ∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) (T : ℕ) : eta gaussNull Es T ≤ ↑(⌈(1 - s ^ 2) / ρ ^ 2⌉₊ + 1) + eta gaussNull (gaussNumeraire s) T

η_T ≤ t_ρ + η'_T for any numéraires Es of Q, with t_ρ = ⌈(1 − s²)/ρ²⌉ + 1 and η'_T the value of the stopping problem of Lemma 2(ii): for t ≥ t_ρ, Es_t = Π_t P_θ-almost surely, so that E_θ(Es_{τ∧T}) ≤ ∑_{t < t_ρ} E_θ(Es_t) + E_θ(Π_{τ∧T}).

The claim of Section 4.3

theorem LogOptimal.sec4_every_rho_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 < ρ → ∀ (Es : ℕ → (ℕ → ℝ) → ENNReal), (∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) → Filter.Tendsto (fun (T : ℕ) => minimaxRegret gaussNull (mixAlt s ρ) Es T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2)) ∧ Filter.Tendsto (fun (T : ℕ) => (eta gaussNull Es T).log / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2))

Proposition 3(i) for every ρ > 0 (Section 4.3): for any numéraires of Q, Γ_T/log log T → 1 − s² (Proposition S5) and log η_T/log log T → 1 − s².

theorem LogOptimal.prop_smallrho_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 < ρ → (LarssonRamdasRufTheorem26 → ∃ (Es : ℕ → (ℕ → ℝ) → ENNReal), ∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) ∧ ∀ (Es : ℕ → (ℕ → ℝ) → ENNReal), (∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) → Filter.Tendsto (fun (T : ℕ) => minimaxRegret gaussNull (mixAlt s ρ) Es T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2)) ∧ Filter.Tendsto (fun (T : ℕ) => (eta gaussNull Es T).log / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2))

Proposition S5, with the existence of numéraires (Larsson, Ramdas and Ruf, 2025, Theorem 2.6): both limits are those of sec4_every_rho_proof.