Basic bounds on the minimax regret

This file proves Proposition 1 (Basic bounds) of the paper, following its proof in Section S1.2, Remark 1, the claim of Section 5 that an upper bound on η_T may replace η_T, and the claim of Section 1 that two e-processes with regrets differing by o(t) have the same limit of t^{-1}E_Q(log E_t).

• Setting.isEProcess_indicator: Proposition 1(i);
• Setting.isEProcess_weighted, Setting.regret_weighted_le, Setting.minimaxRegret_le_log: Proposition 1(ii);
• Setting.one_le_eta, Setting.isEProcess_stopped_div, Setting.regret_div_const, Setting.minimaxRegret_le_log_eta: Proposition 1(iii), for every finite b ≥ η_T in place of η_T;
• Setting.minimaxRegret_eq_zero: Remark 1;
• prop_basic_proof, rem_zero_proof, sec5_upper_bound_proof, and intro_growth_rate_proof.

Proposition 1(i)

theorem LogOptimal.Setting.isEProcess_indicator {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (t : ℕ) : IsEProcess 𝔓 fun (i : ℕ) (x : ℕ → 𝒳) => if t ≤ i then Es t x else 0

Proposition 1(i): the process E_i = E*_t 1(i ≥ t) is an e-process, since E_P(E_τ) = E_P{E*_t 1(τ ≥ t)} ≤ E_P(E*_t) ≤ 1.

Proposition 1(ii)

theorem LogOptimal.Setting.isEProcess_weighted {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {T : ℕ} {ξ : Fin (T + 1) → ℝ} (hξ : ξ ∈ probVectors T) : IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => ∑ i : Fin (T + 1), if ↑i ≤ t then ENNReal.ofReal (ξ i) * Es (↑i) x else 0

Proposition 1(ii): for ξ ∈ Δ_T, the process (∑_{i=0}^{t∧T} ξ_i E*_i)_{t≥0} is an e-process, since E_P(E_τ) ≤ ∑_{i=0}^T ξ_i E_P(E*_i) ≤ 1.

theorem LogOptimal.Setting.regret_weighted_le {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {T : ℕ} {ξ : Fin (T + 1) → ℝ} (hξ : ξ ∈ probVectors T) (t : Fin (T + 1)) : (regret Q (Es ↑t) fun (x : ℕ → 𝒳) => ∑ i : Fin (T + 1), if ↑i ≤ ↑t then ENNReal.ofReal (ξ i) * Es (↑i) x else 0) ≤ (ENNReal.ofReal (ξ t))⁻¹.log

Proposition 1(ii): since E_t ≥ ξ_t E*_t, the regret satisfies R_t(E_t) ≤ log(1/ξ_t).

theorem LogOptimal.Setting.minimaxRegret_le_log {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (T : ℕ) : minimaxRegret 𝔓 Q Es T ≤ ↑(Real.log (↑T + 1))

Proposition 1(ii): the uniform ξ gives Γ_T ≤ log(T + 1).

Proposition 1(iii) and Section 5

theorem LogOptimal.lintegral_le_eta {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Es : ℕ → (ℕ → 𝒳) → ENNReal} {T : ℕ} {P : MeasureTheory.Measure (ℕ → 𝒳)} (hP : P ∈ 𝔓) {τ : (ℕ → 𝒳) → ℕ∞} (hτ : MeasureTheory.IsStoppingTime (dataFiltration 𝒳) τ) : ∫⁻ (x : ℕ → 𝒳), Es (truncTime τ T x) x ∂P ≤ eta 𝔓 Es T

theorem LogOptimal.Setting.one_le_eta {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (T : ℕ) : 1 ≤ eta 𝔓 Es T

Since E*_0 = 1, taking τ = 0 in eq. (4) gives η_T ≥ 1.

theorem LogOptimal.Setting.isEProcess_stopped_div {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {T : ℕ} {b : ENNReal} (hb : eta 𝔓 Es T ≤ b) : IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => Es (min t T) x / b

Proposition 1(iii), for every b ≥ η_T in place of η_T: the process (E*_{t∧T}/b)_{t≥0} is an e-process, since E_τ = E*_{τ∧T}/b, also on the event {τ = ∞}, and E_P(E*_{τ∧T}) ≤ η_T ≤ b.

theorem LogOptimal.Setting.regret_div_const {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (t : ℕ) (b : ENNReal) : (regret Q (Es t) fun (x : ℕ → 𝒳) => Es t x / b) = b.log

Proposition 1(iii), for every b in place of η_T: since 0 < E*_t < ∞ Q-almost surely, E*_t/(E*_t/b) = b Q-almost surely, and the regret of E*_t/b is log b.

theorem LogOptimal.Setting.minimaxRegret_eq_zero {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {T : ℕ} {Es' : ℕ → (ℕ → 𝒳) → ENNReal} (hEs' : ∀ t ≤ T, Es' t =ᵐ[Q] Es t) (hE : IsEProcess 𝔓 fun (t : ℕ) => Es' (min t T)) : minimaxRegret 𝔓 Q Es T = 0

Remark 1: if E*_0, …, E*_T have versions such that (E*_{t∧T})_{t≥0} is an e-process, then Γ_T = 0, since these versions have regret zero and Γ_T ≥ 0.

theorem LogOptimal.Setting.minimaxRegret_le_log_eta {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) (T : ℕ) : minimaxRegret 𝔓 Q Es T ≤ (eta 𝔓 Es T).log

Proposition 1(iii): Γ_T ≤ log η_T, trivially if η_T = ∞.

Proposition 1, Remark 1, and the claims of Sections 1 and 5

theorem LogOptimal.prop_basic_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Setting 𝔓 Q Es → ∀ (T : ℕ), minimaxRegret 𝔓 Q Es T ≤ minimaxRegret 𝔓 Q Es (T + 1) ∧ (∀ (t : ℕ), (IsEProcess 𝔓 fun (i : ℕ) (x : ℕ → 𝒳) => if t ≤ i then Es t x else 0) ∧ regret Q (Es t) (Es t) = 0) ∧ (∀ ξ ∈ probVectors T, (IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => ∑ i : Fin (T + 1), if ↑i ≤ t then ENNReal.ofReal (ξ i) * Es (↑i) x else 0) ∧ ∀ (t : Fin (T + 1)), (regret Q (Es ↑t) fun (x : ℕ → 𝒳) => ∑ i : Fin (T + 1), if ↑i ≤ ↑t then ENNReal.ofReal (ξ i) * Es (↑i) x else 0) ≤ (ENNReal.ofReal (ξ t))⁻¹.log) ∧ minimaxRegret 𝔓 Q Es T ≤ ↑(Real.log (↑T + 1)) ∧ (eta 𝔓 Es T < ⊤ → (IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => Es (min t T) x / eta 𝔓 Es T) ∧ ∀ t ≤ T, (regret Q (Es t) fun (x : ℕ → 𝒳) => Es t x / eta 𝔓 Es T) = (eta 𝔓 Es T).log) ∧ minimaxRegret 𝔓 Q Es T ≤ (eta 𝔓 Es T).log

theorem LogOptimal.rem_zero_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Setting 𝔓 Q Es → ∀ (T : ℕ), (∃ (Es' : ℕ → (ℕ → 𝒳) → ENNReal), (∀ t ≤ T, Measurable (Es' t) ∧ Es' t =ᵐ[Q] Es t) ∧ IsEProcess 𝔓 fun (t : ℕ) => Es' (min t T)) → minimaxRegret 𝔓 Q Es T = 0

theorem LogOptimal.sec5_upper_bound_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Setting 𝔓 Q Es → ∀ (T : ℕ) (b : ENNReal), eta 𝔓 Es T ≤ b → b < ⊤ → (IsEProcess 𝔓 fun (t : ℕ) (x : ℕ → 𝒳) => Es (min t T) x / b) ∧ ∀ t ≤ T, (regret Q (Es t) fun (x : ℕ → 𝒳) => Es t x / b) = b.log

theorem LogOptimal.Setting.toReal_ePower_eq {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) {t : ℕ} (hR : regret Q (Es t) (E t) ≠ ⊤) : (ePower Q (E t)).toReal = ∫ (x : ℕ → 𝒳), (Es t x).log.toReal ∂Q - (regret Q (Es t) (E t)).toReal

For an e-process with finite regrets, E_Q(log E_t) = E_Q(log E*_t) − R_t(E_t) in ℝ, by Lemma S1.

theorem LogOptimal.intro_growth_rate_proof (𝒳 : Type u) [MeasurableSpace 𝒳] (𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))) (Q : MeasureTheory.Measure (ℕ → 𝒳)) (Es : ℕ → (ℕ → 𝒳) → ENNReal) : Setting 𝔓 Q Es → ∀ (E E' : ℕ → (ℕ → 𝒳) → ENNReal), IsEProcess 𝔓 E → IsEProcess 𝔓 E' → (∀ (t : ℕ), regret Q (Es t) (E t) ≠ ⊤) → (∀ (t : ℕ), regret Q (Es t) (E' t) ≠ ⊤) → Filter.Tendsto (fun (t : ℕ) => ((regret Q (Es t) (E t)).toReal - (regret Q (Es t) (E' t)).toReal) / ↑t) Filter.atTop (nhds 0) → Filter.Tendsto (fun (t : ℕ) => ((ePower Q (E t)).toReal - (ePower Q (E' t)).toReal) / ↑t) Filter.atTop (nhds 0)