The e-process of Proposition 3(ii)

This file proves Proposition 3(ii) of the paper, following its proof in Section S1.6, except for the lower bound on the upper limit of the regrets, which also needs the lower bound of Proposition 3(i) and is stated here with that bound as a hypothesis.

Let s ∈ (0, 1), T_j = ⌈exp(e^j)⌉, q_j = 1 + s²/{(1 − s²)(j + 1)}, u_j as in Proposition 3(ii), and c_j = 1/{j(j + 1)u_j}.

• eta_horizon_le_etaBound: Lemma S3 with T = T_j and q = q_j gives η_{T_j} ≤ u_j;
• lintegral_mixtureEProcess_truncTime_le: E_θ(E_{τ∧n}) = ∑_j c_j E_θ(E*_{τ∧n∧T_j}) ≤ 1;
• ae_tendsto_mixtureEProcess: E_t converges almost surely under every P_θ;
• isEProcess_mixtureEProcess: (E_t) is an e-process, by Fatou's lemma;
• regret_mixtureEProcess_le: for t ≤ T_j, E_t ≥ c_j E*_t, so that R_t(E_t) ≤ log u_j + log{j(j + 1)}, for every alternative;
• log_mul_etaBound_le: log{j(j + 1)u_j} ≤ (1 − s²)j + 4 log(j + 2) + C;
• eventually_regret_mixtureEProcess_lt: for every b > 1 − s², eventually R_t(E_t) < b log log t;
• frequently_lt_regret_mixtureEProcess: if Γ_T/log log T has lower limit at least 1 − s², then R_t(E_t)/log log t exceeds every a < 1 − s² infinitely often.

Departures from the paper. The paper shows that E*_t → 0 almost surely under P_θ by the strong law of large numbers, and deduces that E_t converges almost surely. We use instead that the nonnegative martingale (E*_t) with respect to (𝒢_t) (Proposition 2) converges almost surely to a finite limit (Doob's convergence theorem): a finite limit suffices for the convergence of E_t, by dominated convergence for the series over j. For the lower bound on the upper limit, the paper takes a maximizer t_T of R_t(E_t) over t ≤ T; we argue by contradiction with the same inequality Γ_T ≤ max_{t ≤ T} R_t(E_t).

The horizons T_j, the ratios q_j, and the bounds u_j

theorem LogOptimal.one_le_horizon (j : ℕ) : 1 ≤ horizon j

theorem LogOptimal.exp_exp_le_horizon (j : ℕ) : Real.exp (Real.exp ↑j) ≤ ↑(horizon j)

theorem LogOptimal.blockRatio_gt_one {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (j : ℕ) : 1 < blockRatio s j

theorem LogOptimal.one_sub_sq_mul_blockRatio {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (j : ℕ) : (1 - s ^ 2) * blockRatio s j = 1 - s ^ 2 * ↑j / (↑j + 1)

(1 − s²)q_j = 1 − s²j/(j + 1).

theorem LogOptimal.blockRatio_lt {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : blockRatio s j < 1 / (1 - s ^ 2)

theorem LogOptimal.etaBound_pos {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : 0 < etaBound s j

theorem LogOptimal.one_le_etaBound {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : 1 ≤ etaBound s j

u_j ≥ 1, since (j + 1)/(s²j) > 1 and the base is at least 2.

theorem LogOptimal.log_etaBound {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : Real.log (etaBound s j) = (1 - s ^ 2) * blockRatio s j * Real.log (2 + 2 * Real.log ↑(horizon j) / Real.log (blockRatio s j)) + Real.log (1 / (1 - (1 - s ^ 2) * blockRatio s j))

log u_j is the right-hand side of Lemma S3 with T = T_j and q = q_j.

theorem LogOptimal.eta_horizon_le_etaBound {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : eta gaussNull (gaussNumeraire s) (horizon j) ≤ ENNReal.ofReal (etaBound s j)

η_{T_j} ≤ u_j: Lemma S3 with T = T_j and q = q_j.

theorem LogOptimal.ofReal_mul_etaBound_pos {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : ENNReal.ofReal (↑j * (↑j + 1) * etaBound s j) ≠ 0

The denominator j(j + 1)u_j of the weight c_j, in [0, ∞], is positive and finite.

theorem LogOptimal.ofReal_mul_le_ofReal_mul_etaBound {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {j : ℕ} (hj : 1 ≤ j) : ENNReal.ofReal (↑j * (↑j + 1)) ≤ ENNReal.ofReal (↑j * (↑j + 1) * etaBound s j)

j(j + 1)u_j ≥ j(j + 1) in [0, ∞].

The weights 1/{j(j + 1)}

Measurability

theorem LogOptimal.measurable_mixtureEProcess_dataFiltration (s : ℝ) (t : ℕ) : Measurable (mixtureEProcess s t)

The e-process of Proposition 3(ii) is adapted to (ℱ_t).

theorem LogOptimal.measurable_mixtureEProcess_helmertFiltration (s : ℝ) (t : ℕ) : Measurable (mixtureEProcess s t)

Each term of the e-process of Proposition 3(ii) is a function of Y^t: it is measurable with respect to 𝒢_t.

The e-process property

theorem LogOptimal.lintegral_mixtureEProcess_truncTime_le {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (θ : ℝ) {τ : (ℕ → ℝ) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration ℝ) τ) (n : ℕ) : ∫⁻ (x : ℕ → ℝ), mixtureEProcess s (truncTime τ n x) x ∂nullDist θ ≤ 1

E_θ(E_{τ∧n}) = ∑_j c_j E_θ(E*_{τ∧n∧T_j}) ≤ ∑_j c_j η_{T_j} ≤ ∑_j 1/{j(j + 1)} ≤ 1.

theorem LogOptimal.ae_tendsto_mixtureEProcess {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (θ : ℝ) : ∀ᵐ (x : ℕ → ℝ) ∂nullDist θ, Filter.Tendsto (fun (t : ℕ) => mixtureEProcess s t x) Filter.atTop (nhds (∑' (j : ℕ), if j = 0 then 0 else gaussNumeraire s (horizon j) x / ENNReal.ofReal (↑j * (↑j + 1) * etaBound s j)))

E_t converges almost surely under every P_θ: the terms c_j E*_{t∧T_j} converge, and they are dominated by c_j sup_t E*_t, which is summable since E*_t converges to a finite limit.

theorem LogOptimal.isEProcess_mixtureEProcess {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) : IsEProcess gaussNull (mixtureEProcess s)

Proposition 3(ii), the e-process property: for every θ and every stopping time τ, E_θ(E_{τ∧n}) ≤ 1, E_{τ∧n} → E_τ almost surely, and Fatou's lemma gives E_θ(E_τ) ≤ 1.

The regret of the e-process

theorem LogOptimal.regret_mixtureEProcess_le {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (Q : MeasureTheory.Measure (ℕ → ℝ)) [MeasureTheory.IsProbabilityMeasure Q] {t j : ℕ} (hj : 1 ≤ j) (htj : t ≤ horizon j) : regret Q (gaussNumeraire s t) (mixtureEProcess s t) ≤ ↑(Real.log (↑j * (↑j + 1) * etaBound s j))

For t ≤ T_j with j ≥ 1, E_t ≥ c_j E*_t, so that E*_t/E_t ≤ j(j + 1)u_j and R_t(E_t) ≤ log{j(j + 1)u_j}, for every alternative Q.

theorem LogOptimal.eventually_regret_mixtureEProcess_lt {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (Q : MeasureTheory.Measure (ℕ → ℝ)) [MeasureTheory.IsProbabilityMeasure Q] {b : ℝ} (hb : 1 - s ^ 2 < b) : ∀ᶠ (t : ℕ) in Filter.atTop, regret Q (gaussNumeraire s t) (mixtureEProcess s t) < ↑(b * Real.log (Real.log ↑t))

For every b > 1 − s², eventually R_t(E_t) < b log log t: the upper bound in Proposition 3(ii), for every alternative Q.

theorem LogOptimal.frequently_lt_regret_mixtureEProcess {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (Q : MeasureTheory.Measure (ℕ → ℝ)) [MeasureTheory.IsProbabilityMeasure Q] (hlow : ∀ a < 1 - s ^ 2, ∀ᶠ (T : ℕ) in Filter.atTop, ↑(a * Real.log (Real.log ↑T)) < minimaxRegret gaussNull Q (gaussNumeraire s) T) {a : ℝ} (ha : a < 1 - s ^ 2) : ∃ᶠ (t : ℕ) in Filter.atTop, ↑a < regret Q (gaussNumeraire s t) (mixtureEProcess s t) / ↑(Real.log (Real.log ↑t))

The lower bound on the upper limit in Proposition 3(ii): if, for every a < 1 − s², eventually a log log T < Γ_T, then R_t(E_t)/log log t exceeds every a < 1 − s² infinitely often. Otherwise R_t(E_t) ≤ a log log t for t ≥ t₀, and Γ_T ≤ max_{t ≤ T} R_t(E_t) stays below C + a log log T.