The claims of Section S2.3

This file completes the claims of Section S2.3 of the supplementary material that follow Proposition S2, following the paper: 'Moreover, the null distributions of X² are absolutely continuous with respect to Q₂. For s ≠ 1, Proposition S1(i) and (S16) therefore give Γ₂ > 0, and Proposition 1 gives Γ_T ≥ Γ₂ > 0 for every T ≥ 2.' The setting of Sections 1 and 2 for the Gaussian location model is Proposition 2 (setting_gaussNumeraire_mixAlt), and Proposition S1(i) is Setting.exists_isEProcess_versions.

• minimaxRegret_gaussNumeraire_pos: Γ_T > 0 for s ≠ 1 and T ≥ 2;
• sec_notep_proof: the statement sec_notep.

theorem LogOptimal.minimaxRegret_gaussNumeraire_pos {s ρ : ℝ} (hs : 0 < s) (hs1 : s ≠ 1) (hρ : 1 - s ^ 2 ≤ ρ ^ 2) (T : ℕ) : 2 ≤ T → 0 < minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T

Positivity of the minimax regret (Section S2.3): for s ≠ 1 and ρ² ≥ 1 − s², Γ_T ≥ Γ₂ > 0 for every T ≥ 2, by Proposition S1(i), eq. (S16), and Proposition 1.

theorem LogOptimal.sec_notep_proof (s ρ : ℝ) : 0 < s → s ≠ 1 → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → (∀ (θ : ℝ) (x : ℕ → ℝ), 1 < notepCond s θ x ↔ if s < 1 then (x 0 - θ) ^ 2 < (1 + s ^ 2) / (1 - s ^ 2) * Real.log (2 / (1 + s ^ 2)) else (1 + s ^ 2) / (1 - s ^ 2) * Real.log (2 / (1 + s ^ 2)) < (x 0 - θ) ^ 2) ∧ ¬IsEProcess gaussNull (gaussNumeraire s) ∧ (∀ P ∈ gaussNull, (marginal P 2).AbsolutelyContinuous (marginal (mixAlt s ρ) 2)) ∧ ∀ (T : ℕ), 2 ≤ T → 0 < minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T