Theorem 1, the growth of the minimax regret, and the frontier

This file proves Theorem 1 of the paper (Composite alternative), following its proof in Section S1.7, the claims of Section 4.3 on the growth of the minimax regret in the worst case over μ, the frontier of Section 1, and the claim of Section S2.5 on when Γ_T tends to infinity. The lower bound (S9) is Lemma S6 (lem_fixedk_proof).

• isEProcess_ite_zero_one: replacing E_0 by 1 preserves the e-process property, since every stopping time τ of (ℱ_t) satisfies τ = 0 everywhere or τ ≥ 1 everywhere;
• kappa_add_regret_le_iSup_regret_altDist: for t ≥ 1 and E ∈ ℰ_t, sup_μ R^μ_t(E) ≥ ∫ R^μ_t(E) N(0, ρ²)(dμ) = tκ − E_Q(log E) = κ + R_t(E), the averaging step of the proof of Theorem 1(i), done separately for the positive and negative parts of log E;
• kappa_add_minimaxRegret_le_worstCase and worstCase_le_kappa_add_log_eta: the two inequalities of Theorem 1(i);
• thm_composite_proof: Theorem 1;
• sec4_growth_proof, intro_frontier_proof, sec_frontier_proof: the claims of Sections 4.3, 1, and S2.5.

In the averaging step, the paper computes the average of R^μ_t(E) over μ; we show instead that R^μ_t(E) ≤ r for every μ implies κ + R_t(E) ≤ r, by averaging the e-powers E_{Q_μ}(log E) ≥ tκ − r, which is the same computation with a bound in place of the average.

Replacing E_0 by one

theorem LogOptimal.isEProcess_ite_zero_one {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} (h𝔓 : ∀ P ∈ 𝔓, MeasureTheory.IsProbabilityMeasure P) {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) : IsEProcess 𝔓 fun (t : ℕ) => if t = 0 then fun (x : ℕ → 𝒳) => 1 else E t

Replacing E_0 by 1 preserves the e-process property (proof of Theorem 1): since ℱ₀ is trivial, every stopping time τ satisfies τ = 0 everywhere, so that E_τ = 1, or τ ≥ 1 everywhere, so that E_τ is unchanged.

The averaging step of the proof of Theorem 1(i)

theorem LogOptimal.kappa_add_regret_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 (mixAlt s ρ) (gaussNumeraire s t) E ≤ ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) E

The averaging step of the proof of Theorem 1(i): for s ≤ 1, t ≥ 1, and E ∈ ℰ_t, κ + R_t(E) ≤ sup_μ R^μ_t(E). If R^μ_t(E) = tκ − E_{Q_μ}(log E) ≤ r for every μ, then E_{Q_μ}(log E) ≥ tκ − r, the average over μ ∼ N(0, ρ²) gives E_Q(log E) ≥ tκ − r, and R_t(E) = (t − 1)κ − E_Q(log E) ≤ r − κ.

Theorem 1(i)

theorem LogOptimal.kappa_add_minimaxRegret_le_worstCase {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {ρ : ℝ} (hρ : 1 - s ^ 2 ≤ ρ ^ 2) {Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal} (hEsμ : ∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) {T : ℕ} (hT : 1 ≤ T) : ↑(kappa s) + minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T ≤ worstCaseMinimaxRegret s Esμ T

Theorem 1(i), lower bound: κ + Γ_T ≤ inf_{(E_t)} max_{0≤t≤T} sup_μ R^μ_t(E_t) for T ≥ 1.

theorem LogOptimal.worstCase_le_kappa_add_log_eta {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) {ρ : ℝ} (hρ : 1 - s ^ 2 ≤ ρ ^ 2) {Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal} (hEsμ : ∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) (T : ℕ) : worstCaseMinimaxRegret s Esμ T ≤ ↑(kappa s) + (eta gaussNull (gaussNumeraire s) T).log

Theorem 1(i), upper bound: inf_{(E_t)} max_{0≤t≤T} sup_μ R^μ_t(E_t) ≤ κ + log η_T, with the e-process (E*_{t∧T}/η_T)_{t≥0} of Proposition 1(iii), whose terms are functions of the Y_i.

Theorem 1

theorem LogOptimal.thm_composite_proof (s ρ : ℝ) : 0 < s → s < 1 → 0 ≤ ρ → 1 - s ^ 2 ≤ ρ ^ 2 → ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → ((∀ (T : ℕ), 1 ≤ T → ↑(kappa s) + minimaxRegret gaussNull (mixAlt s ρ) (gaussNumeraire s) T ≤ worstCaseMinimaxRegret s Esμ T ∧ worstCaseMinimaxRegret s Esμ T ≤ ↑(kappa s) + (eta gaussNull (gaussNumeraire s) T).log) ∧ Filter.Tendsto (fun (T : ℕ) => worstCaseMinimaxRegret s Esμ T / ↑(Real.log (Real.log ↑T))) Filter.atTop (nhds ↑(1 - s ^ 2))) ∧ (∀ (t : ℕ), 1 ≤ t → ⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) (mixtureEProcess s t) = ↑(kappa s) + regret (mixAlt s ρ) (gaussNumeraire s t) (mixtureEProcess s t)) ∧ Filter.limsup (fun (t : ℕ) => (⨆ (μ : ℝ), regret (altDist s μ) (Esμ μ t) (mixtureEProcess s t)) / ↑(Real.log (Real.log ↑t))) Filter.atTop = ↑(1 - s ^ 2)

Theorem 1.

The growth of the minimax regret and the frontier

theorem LogOptimal.sec4_growth_proof (s : ℝ) : 0 < s → s < 1 → ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → Filter.Tendsto (worstCaseMinimaxRegret s Esμ) Filter.atTop (nhds ⊤) ∧ ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (T : ℕ) => worstCaseMinimaxRegret s Esμ T / ↑(Real.log ↑T ^ ε)) Filter.atTop (nhds 0)

The growth of the minimax regret (Section 4.3): Theorem 1 with ρ = 1 shows that the minimax regret in the worst case over μ tends to infinity, and its upper bound κ + log η_T grows like log log T, more slowly than any power of log T.

theorem LogOptimal.exists_minimaxRegret_altDist_le {s : ℝ} (hs : 0 < s) (μ : ℝ) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hEs : ∀ (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Es t)) : ∃ (C : ℝ), ∀ (T : ℕ), minimaxRegret gaussNull (altDist s μ) Es T ≤ ↑C

For the alternatives Q_μ, with any numéraires, the minimax regret is bounded: it is zero for s ≤ 1 and at most log s for s > 1 (Proposition S4).

theorem LogOptimal.intro_frontier_proof (s : ℝ) : 0 < s → ∀ (Esμ : ℝ → ℕ → (ℕ → ℝ) → ENNReal), (∀ (μ : ℝ) (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Esμ μ t)) → ((∃ (C : ℝ), ∀ (T : ℕ), worstCaseMinimaxRegret s Esμ T ≤ ↑C) ↔ 1 ≤ s)

The frontier of the Gaussian location problem (Section 1), from the statement of Lemma S6: the minimax regret in the worst case over μ is bounded if and only if s ≥ 1.

theorem LogOptimal.sec_frontier_proof : (∀ (s μ : ℝ), 0 < s → ∀ (Es : ℕ → (ℕ → ℝ) → ENNReal), (∀ (t : ℕ), IsNumeraire gaussNull (altDist s μ) t (Es t)) → ¬Filter.Tendsto (minimaxRegret gaussNull (altDist s μ) Es) Filter.atTop (nhds ⊤)) ∧ ∀ (s ρ : ℝ), 0 < s → 0 ≤ ρ → ∀ (Es : ℕ → (ℕ → ℝ) → ENNReal), (∀ (t : ℕ), IsNumeraire gaussNull (mixAlt s ρ) t (Es t)) → (Filter.Tendsto (minimaxRegret gaussNull (mixAlt s ρ) Es) Filter.atTop (nhds ⊤) ↔ s < 1 ∧ 0 < ρ)

When the minimax regret tends to infinity (Section S2.5): for the alternatives Q_μ, Γ_T is bounded (Proposition S4); for the mixtures, Γ_T → ∞ exactly when s < 1 and ρ > 0, by Proposition S5, by Proposition 4 for s ≥ 1, and by Proposition S4 for ρ = 0.