Proposition S4, the regret against Q_μ, and the minimax regret at a single horizon

This file proves Proposition S4 (Insufficiency of a simple Gaussian alternative) of the supplementary material, following its proof in Section S2.5, the claims of Section S2.5 on the measure P*_t of Q_μ, and the claims of Section 4 on the worst case over the location μ at a single horizon, following the proof of Theorem 1 in Section S1.7.

• condExp_lik_sub_comp_ae_eq: under P_θ and for s ≤ 1, given ℱ_t, the conditional expectation of ℓ(X_{t+1} − C) for an ℱ_t-measurable C = c(X^t) is exp{−(1 − s²)(θ − C)²/2}, by eq. (S1) with v = 1, since X_{t+1} ∼ N(θ, 1) is independent of ℱ_t;
• isTestSupermartingale_likProcess: for s ≤ 1, (∏_{i=1}^t ℓ(X_i − μ))_{t≥0} is a test supermartingale with respect to (ℱ_t);
• isNumeraire_likProcess_altDist: for s ≤ 1, ∏_{i=1}^t ℓ(X_i − μ) = dQ_{μ,t}/dP_{μ,t} is the numéraire of Q_μ;
• isNumeraire_gaussNumeraire_altDist: for s ≥ 1, E*_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire of every Q_μ, with P*_t = ∫ P_{θ,t} N{μ, (s² − 1)/t}(dθ);
• prop_simple_proof (Proposition S4) and sec_simple_proof (Section S2.5);
• ePower_altDist_eq_ePower_mixAlt: the e-power of an e-variable that is a function of Y_2, …, Y_t is the same under every Q_μ and under Q, since the distribution of Y^t is;
• regret_altDist_eq_kappa_add: partial result 3, the identity R^μ_t(E) = κ + R_t(E) of the proof of Theorem 1(ii) for such an e-variable and s ≤ 1, with R^μ_t defined by any numéraires of Q_μ;
• sec4_worst_case_average_proof and sec4_single_horizon_proof: the worst case over μ is at least the average under N(0, ρ²), and the minimax regret at a single horizon in the worst case over μ is κ, attained by E*_t.

The conditional expectation of ℓ(X_{t+1} − C)

theorem LogOptimal.lik_le_inv {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (y : ℝ) : lik s y ≤ s⁻¹

For s ≤ 1, ℓ(y) ≤ s^{−1}.

theorem LogOptimal.integral_lik_sub_gaussianReal {s : ℝ} (hs : 0 < s) (θ c : ℝ) : ∫ (y : ℝ), lik s (y - c) ∂ProbabilityTheory.gaussianReal θ 1 = Real.exp (-((1 - s ^ 2) * (θ - c) ^ 2) / 2)

E{ℓ(Z − c)} = exp{−(1 − s²)(θ − c)²/2} for Z ∼ N(θ, 1), by eq. (S1) with v = 1.

theorem LogOptimal.condExp_lik_sub_comp_ae_eq {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (θ : ℝ) (t : ℕ) {c : (Fin t → ℝ) → ℝ} (hc : Measurable c) : (nullDist θ)[fun (x : ℕ → ℝ) => lik s (x t - c fun (i : Fin t) => x ↑i) | ↑(dataFiltration ℝ) t] =ᵐ[nullDist θ] fun (x : ℕ → ℝ) => Real.exp (-((1 - s ^ 2) * (θ - c fun (i : Fin t) => x ↑i) ^ 2) / 2)

The conditional expectation of ℓ(X_{t+1} − C) (proofs of Propositions S4(i) and S6): under P_θ and for s ≤ 1, given ℱ_t, the conditional expectation of ℓ(X_{t+1} − c(X^t)) is exp{−(1 − s²)(θ − c(X^t))²/2}, since X_{t+1} ∼ N(θ, 1) is independent of ℱ_t.

Proposition S4(i): s ≤ 1

theorem LogOptimal.likProcess_le_inv_pow {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (μ : ℝ) (t : ℕ) (x : ℕ → ℝ) : likProcess s μ t x ≤ s⁻¹ ^ t

theorem LogOptimal.isTestSupermartingale_likProcess {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (μ : ℝ) : IsTestSupermartingale gaussNull (dataFiltration ℝ) (likProcess s μ)

Proposition S4(i), test supermartingale: for s ≤ 1, the factors of ∏_{i=1}^t ℓ(X_i − μ) satisfy E_θ{ℓ(X_i − μ)} = exp{−(1 − s²)(θ − μ)²/2} ≤ 1 and are independent under every P_θ, so that the product is a test supermartingale with respect to (ℱ_t).

theorem LogOptimal.isNumeraire_likProcess_altDist {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (μ : ℝ) (t : ℕ) : IsNumeraire gaussNull (altDist s μ) t fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)

Proposition S4(i), numéraire: for s ≤ 1, ∏_{i=1}^t ℓ(X_i − μ) = dQ_{μ,t}/dP_{μ,t} is an e-variable, and E_{Q_μ}(E/∏_{i=1}^t ℓ(X_i − μ)) = E_μ(E) ≤ 1 for every E ∈ ℰ_t since P_μ ∈ 𝒫; it is therefore the numéraire of Q_μ, with P*_t = P_{μ,t}.

theorem LogOptimal.setting_likProcess_altDist {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (μ : ℝ) : Setting gaussNull (altDist s μ) fun (t : ℕ) (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)

For s ≤ 1, the numéraires ∏_{i=1}^t ℓ(X_i − μ) give the setting of Sections 1 and 2 for the alternative Q_μ.

theorem LogOptimal.eta_likProcess_le_one {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (μ : ℝ) (T : ℕ) : eta gaussNull (fun (t : ℕ) (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) T ≤ 1

For s ≤ 1, η_T ≤ 1 for the numéraires of Q_μ, by optional stopping for the test supermartingale (∏_{i=1}^t ℓ(X_i − μ))_{t≥0}.

Proposition S4(ii): s ≥ 1

theorem LogOptimal.isNumeraire_gaussNumeraire_altDist {s : ℝ} (hs : 1 ≤ s) (μ : ℝ) (t : ℕ) : IsNumeraire gaussNull (altDist s μ) t (gaussNumeraire s t)

Proposition S4(ii), numéraire: for s ≥ 1, E*_t = ∏_{i=2}^t ℓ(Y_i) is the numéraire of every Q_μ at every horizon t ≥ 0, with P*_t = ∫ P_{θ,t} N{μ, (s² − 1)/t}(dθ) for t ≥ 1.

theorem LogOptimal.setting_gaussNumeraire_altDist {s : ℝ} (hs : 1 ≤ s) (μ : ℝ) : Setting gaussNull (altDist s μ) (gaussNumeraire s)

theorem LogOptimal.log_eta_gaussNumeraire_le_log {s : ℝ} (hs : 1 ≤ s) (T : ℕ) : (eta gaussNull (gaussNumeraire s) T).log ≤ ↑(Real.log s)

For s ≥ 1, log η_T ≤ log s, since η_T = sup_τ E(h_{τ∧T}) (Lemma 2(ii)) and h_t ≤ s.

Proposition S4 and Section S2.5

theorem LogOptimal.prop_simple_proof (s μ : ℝ) : 0 < s → ∀ (T : ℕ), (s ≤ 1 → (∀ (t : ℕ), IsNumeraire gaussNull (altDist s μ) t fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) ∧ (∀ (t : ℕ), (ePower (altDist s μ) fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) = ↑(↑t * kappa s)) ∧ IsTestSupermartingale gaussNull (dataFiltration ℝ) (likProcess s μ) ∧ minimaxRegret gaussNull (altDist s μ) (fun (t : ℕ) (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) T = 0) ∧ (1 < s → (∀ (t : ℕ), 1 ≤ t → IsNumeraire gaussNull (altDist s μ) t (gaussNumeraire s t)) ∧ minimaxRegret gaussNull (altDist s μ) (gaussNumeraire s) T ≤ (eta gaussNull (gaussNumeraire s) T).log ∧ (eta gaussNull (gaussNumeraire s) T).log ≤ ↑(Real.log s))

theorem LogOptimal.sec_simple_proof : (∀ (s μ : ℝ), 0 < s → s ≤ 1 → ∀ (t : ℕ), (IsNumeraire gaussNull (altDist s μ) t fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) ∧ IsNumeraireDensity (altDist s μ) t (fun (x : ℕ → ℝ) => ENNReal.ofReal (likProcess s μ t x)) (marginal (nullDist μ) t)) ∧ (∀ (s ρ : ℝ), (∀ (t : ℕ), 1 ≤ t → 0 ≤ ρ ^ 2 - (1 - s ^ 2) / ↑t) ↔ 1 - s ^ 2 ≤ ρ ^ 2) ∧ (∀ (s : ℝ), mixAlt s 0 = altDist s 0) ∧ ∀ (s : ℝ), 0 < s → (1 - s ^ 2 ≤ 0 ^ 2 ↔ 1 ≤ s)

Functions of Y_2, …, Y_t under Q_μ and under Q

theorem LogOptimal.helmertFiltration_le_comap_helmertVec (t : ℕ) : ↑helmertFiltration t ≤ MeasurableSpace.comap (helmertVec t) MeasurableSpace.pi

theorem LogOptimal.lintegral_altDist_eq_lintegral_mixAlt (s μ ρ : ℝ) {t : ℕ} (ht : 1 ≤ t) {f : (ℕ → ℝ) → ENNReal} (hf : Measurable f) : ∫⁻ (x : ℕ → ℝ), f x ∂altDist s μ = ∫⁻ (x : ℕ → ℝ), f x ∂mixAlt s ρ

The expectation of a function of Y_2, …, Y_t is the same under every Q_μ and under Q, since Y^t ∼ N(0, s²)^{⊗(t−1)} under each of them.

theorem LogOptimal.ePower_altDist_eq_ePower_mixAlt (s μ ρ : ℝ) {t : ℕ} (ht : 1 ≤ t) {E : (ℕ → ℝ) → ENNReal} (hE : Measurable E) : ePower (altDist s μ) E = ePower (mixAlt s ρ) E

The e-power of a function of Y_2, …, Y_t is the same under every Q_μ and under Q.

theorem LogOptimal.measurable_gaussNumeraire_helmertFiltration_le (s : ℝ) (t : ℕ) : Measurable (gaussNumeraire s t)

theorem LogOptimal.ePower_numeraire_altDist {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (μ : ℝ) {t : ℕ} {Es : (ℕ → ℝ) → ENNReal} (hEs : IsNumeraire gaussNull (altDist s μ) t Es) : ePower (altDist s μ) Es = ↑(↑t * kappa s)

For s ≤ 1, the numéraires of Q_μ have e-power tκ, since they equal ∏_{i=1}^t ℓ(X_i − μ) Q_μ-almost surely.

theorem LogOptimal.regret_mixAlt_gaussNumeraire_eq {s : ℝ} (hs : 0 < s) (ρ : ℝ) {t : ℕ} {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) : regret (mixAlt s ρ) (gaussNumeraire s t) E = ↑(↑(t - 1) * kappa s) - ePower (mixAlt s ρ) E

For every ρ, t ≥ 1, and E ∈ ℰ_t, R_t(E) = (t − 1)κ − E_Q(log E) for the regret against E*_t = ∏_{i=2}^t ℓ(Y_i) under the mixture Q.

theorem LogOptimal.regret_altDist_eq_kappa_add {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (ρ : ℝ) {Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal} (hEsμ : ∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) {t : ℕ} (ht : 1 ≤ t) {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) (hEY : Measurable E) (μ : ℝ) : regret (altDist s μ) (Esμ μ t) E = ↑(kappa s) + regret (mixAlt s ρ) (gaussNumeraire s t) E

Partial result 3 (proof of Theorem 1(ii), Section S1.7): for s ≤ 1, every ρ, t ≥ 1, and an e-variable E ∈ ℰ_t that is a function of Y_2, …, Y_t, R^μ_t(E) = κ + R_t(E) for every μ, where R^μ_t is the regret against any numéraire of Q_μ and R_t the regret against E*_t = ∏_{i=2}^t ℓ(Y_i) under Q. Indeed, E_{Q_μ}(log E) = E_Q(log E), while the numéraires of Q_μ and of Q have the e-powers tκ and (t − 1)κ.

theorem LogOptimal.iSup_regret_altDist_eq_kappa_add {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (ρ : ℝ) {Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal} (hEsμ : ∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) {t : ℕ} (ht : 1 ≤ t) {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) (hEY : Measurable E) : ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) E = ↑(kappa s) + regret (mixAlt s ρ) (gaussNumeraire s t) E

Partial result 3, in the worst case over μ: sup_μ R^μ_t(E) = κ + R_t(E).

The worst case over the location at a single horizon

theorem LogOptimal.sec4_worst_case_average_proof (s ρ : ℝ) : 0 < s → 0 ≤ ρ → ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → ∀ (t : ℕ) (E : (ℕ → ℝ) → ENNReal), (eIntegral (ProbabilityTheory.gaussianReal 0 (ρ ^ 2).toNNReal) fun (μ : ℝ) => regret (altDist s μ) (Esμ μ t) E) ≤ ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) E

theorem LogOptimal.kappa_le_iSup_regret_altDist {s : ℝ} (hs : 0 < s) (hs1 : s < 1) {Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal} (hEsμ : ∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) {t : ℕ} (ht : 1 ≤ t) {E : (ℕ → ℝ) → ENNReal} (hE : IsEVariable gaussNull t E) : ↑(kappa s) ≤ ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) E

For s < 1 and t ≥ 1, every E ∈ ℰ_t has sup_μ R^μ_t(E) ≥ κ: otherwise E would have an e-power above (t − 1)κ under every Q_μ, hence under Q = ∫ Q_μ N(0, 1)(dμ), against the log-optimality of E*_t for Q.

theorem LogOptimal.sec4_single_horizon_proof (s : ℝ) : 0 < s → s < 1 → ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → ∀ (t : ℕ), 1 ≤ t → ⨅ (E : (ℕ → ℝ) → ENNReal), ⨅ (_ : IsEVariable gaussNull t E), ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) E = ↑(kappa s) ∧ ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) (gaussNumeraire s t) = ↑(kappa s)