Regret bound for the Explore-Then-Commit algorithm

theorem Bandits.ETC.probReal_sumRewards_le_sumRewards_le {K : ℕ} [NeZero K] {m : ℕ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (a : Fin K) : P.real {ω : Ω | Learning.sumRewards A R (bestArm ν) (K * m) ω ≤ Learning.sumRewards A R a (K * m) ω} ≤ Real.exp (-↑m * gap ν a ^ 2 / (4 * ↑σ2))

theorem Bandits.ETC.prob_arm_mul_eq_le {K : ℕ} [NeZero K] {m : ℕ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (a : Fin K) (hm : m ≠ 0) : P.real {ω : Ω | A (K * m) ω = a} ≤ Real.exp (-↑m * gap ν a ^ 2 / (4 * ↑σ2))

The probability that at time K * m the ETC algorithm chooses arm a is at most exp(- m * Δ_a^2 / (4 * σ2)).

theorem Bandits.ETC.expectation_pullCount_le {K : ℕ} [NeZero K] {m : ℕ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) : ∫ (x : Ω), (fun (ω : Ω) => ↑(Learning.pullCount A a n ω)) x ∂P ≤ ↑m + (↑n - ↑K * ↑m) * Real.exp (-↑m * gap ν a ^ 2 / (4 * ↑σ2))

Bound on the expectation of the number of pulls of each arm by the ETC algorithm.

theorem Bandits.ETC.regret_le {K : ℕ} [NeZero K] {m : ℕ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hm : m ≠ 0) (n : ℕ) (hn : K * m ≤ n) : ∫ (x : Ω), regret ν A n x ∂P ≤ ∑ a : Fin K, gap ν a * (↑m + (↑n - ↑K * ↑m) * Real.exp (-↑m * gap ν a ^ 2 / (4 * ↑σ2)))

Regret bound for the ETC algorithm.