Proposition S6: a test supermartingale with the running mean

This file proves Proposition S6 of the supplementary material, following its proof in Section S2.6: the process Ẽ_t = ∏_{i=2}^t ℓ(X_i − X̄_{i−1}) replaces the unknown mean θ in the likelihood ratio L^θ_t by the running mean.

• isTestSupermartingale_runningMeanProduct: for s ≤ 1, (Ẽ_t) is a test supermartingale with respect to (ℱ_t) under every P_θ, since, given ℱ_{i−1}, X_i − X̄_{i−1} is normal with mean θ − X̄_{i−1} and variance one, and eq. (S1) with v = 1 gives E_θ{ℓ(X_i − X̄_{i−1}) ∣ ℱ_{i−1}} = exp{−(1 − s²)(θ − X̄_{i−1})²/2} ≤ 1;
• sub_runningMean_eq_mul_helmertY: X_i − X̄_{i−1} = {i/(i − 1)}^{1/2} Y_i;
• regret_runningMeanProcess_eq: R_t(Ẽ_t) = {(1 − s²)/2} ∑_{i=1}^{t−1} i^{−1}, from log ℓ(y) − log ℓ[{i/(i − 1)}^{1/2} y] = by²/(2i − 2), E_Q(Y_i²) = s², and bs² = 1 − s²;
• prop_plugin_proof: Proposition S6, with the bound Γ_T ≤ {(1 − s²)/2}(1 + log T) from ∑_{i=1}^{T−1} i^{−1} ≤ 1 + log T, and R^μ_t(Ẽ_t) = κ + R_t(Ẽ_t) from the identity of the proof of Theorem 1(ii) (regret_altDist_eq_kappa_add), since Ẽ_t is a function of Y_2, …, Y_t.

The test supermartingale

theorem LogOptimal.isTestSupermartingale_runningMeanProduct {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : IsTestSupermartingale gaussNull (dataFiltration ℝ) fun (t : ℕ) (x : ℕ → ℝ) => ∏ i ∈ Finset.Icc 2 t, lik s (x (i - 1) - runningMean (i - 1) x)

Proposition S6, test supermartingale: for s ≤ 1, Ẽ_t = ∏_{i=2}^t ℓ(X_i − X̄_{i−1}) defines a test supermartingale with respect to (ℱ_t) under every P_θ.

theorem LogOptimal.isEProcess_runningMeanProcess {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : IsEProcess gaussNull (runningMeanProcess s)

For s ≤ 1, (Ẽ_t) is an e-process.

The regret of Ẽ_t

theorem LogOptimal.sub_runningMean_eq_mul_helmertY {i : ℕ} (hi : 2 ≤ i) (x : ℕ → ℝ) : x (i - 1) - runningMean (i - 1) x = (√((↑i - 1) / ↑i))⁻¹ * helmertY i x

X_i − X̄_{i−1} = {i/(i − 1)}^{1/2} Y_i for i ≥ 2, by eq. (7).

theorem LogOptimal.runningMeanProcess_eq (s : ℝ) (t : ℕ) (x : ℕ → ℝ) : runningMeanProcess s t x = ENNReal.ofReal (∏ i ∈ Finset.Icc 2 t, lik s ((√((↑i - 1) / ↑i))⁻¹ * helmertY i x))

Ẽ_t = ∏_{i=2}^t ℓ[{i/(i − 1)}^{1/2} Y_i], a function of Y_2, …, Y_t.

theorem LogOptimal.measurable_runningMeanProcess_helmertFiltration (s : ℝ) (t : ℕ) : Measurable (runningMeanProcess s t)

theorem LogOptimal.regret_runningMeanProcess_eq {s : ℝ} (hs : 0 < s) (ρ : ℝ) {t : ℕ} (ht : 1 ≤ t) : regret (mixAlt s ρ) (gaussNumeraire s t) (runningMeanProcess s t) = ↑((1 - s ^ 2) / 2 * ∑ i ∈ Finset.Icc 1 (t - 1), (↑i)⁻¹)

Proposition S6, regret: for t ≥ 1, R_t(Ẽ_t) = {(1 − s²)/2} ∑_{i=1}^{t−1} i^{−1}.

Proposition S6

theorem LogOptimal.prop_plugin_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → (IsTestSupermartingale gaussNull (dataFiltration ℝ) fun (t : ℕ) (x : ℕ → ℝ) => ∏ i ∈ Finset.Icc 2 t, lik s (x (i - 1) - runningMean (i - 1) x)) ∧ (∀ (t : ℕ), 1 ≤ t → regret (mixAlt s ρ) (gaussNumeraire s t) (runningMeanProcess s t) = ↑((1 - s ^ 2) / 2 * ∑ i ∈ Finset.Icc 1 (t - 1), (↑i)⁻¹)) ∧ (∀ (T : ℕ), 1 ≤ T → minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T ≤ ↑((1 - s ^ 2) / 2 * (1 + Real.log ↑T))) ∧ ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → ∀ (μ : ℝ) (t : ℕ), 1 ≤ t → regret (altDist s μ) (Esμ μ t) (runningMeanProcess s t) = ↑(kappa s) + regret (mixAlt s ρ) (gaussNumeraire s t) (runningMeanProcess s t)