The Explore-Then-Commit Algorithm

noncomputable def Bandits.ETC.nextArm (K : ℕ) [NeZero K] (m n : ℕ) (h : Learning.Hist Unit (Fin K) ℝ n) : Fin K

Arm pulled by the ETC algorithm at time n, as a function of the history before n. For n < K * m, this is arm n % K. For n = K * m, this is the arm with the highest empirical mean after the exploration phase. For n > K * m, this is the same arm as at time n - 1.

Equations

• Bandits.ETC.nextArm K m n h = if hn : n < K * m then Learning.RoundRobin.nextAction K n else if hn_eq : n = K * m then argmax (Learning.empMean' n h) else (h ⟨n - 1, ⋯⟩).action

theorem Bandits.ETC.measurable_nextArm {K : ℕ} [NeZero K] (m n : ℕ) : Measurable (nextArm K m n)

The next arm pulled by ETC is chosen in a measurable way.

noncomputable def Bandits.etcAlgorithm (K : ℕ) [NeZero K] (m : ℕ) : Learning.Algorithm Unit (Fin K) ℝ

The Explore-Then-Commit algorithm: deterministic algorithm that chooses the next arm according to ETC.nextArm.

Equations

• Bandits.etcAlgorithm K m = Learning.detAlgorithm (fun (n : ℕ) (p : Learning.Hist Unit (Fin K) ℝ n × Unit) => Bandits.ETC.nextArm K m n p.1) ⋯

theorem Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) : Learning.IsAlgEnvSeqUntil O A R (Learning.roundRobinAlgorithm K) (Learning.stationaryEnv ν) P (K * m)

Before round K * m, the ETC algorithm behaves like the Round-Robin algorithm.

theorem Bandits.ETC.arm_ae_eq_nextArm {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (n : ℕ) : A n =ᵐ[P] fun (ω : Ω) => nextArm K m n (Learning.history O A R n ω)

theorem Bandits.ETC.arm_of_lt {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) {n : ℕ} (hn : n < K * m) : A n =ᵐ[P] fun (x : Ω) => Learning.RoundRobin.nextAction K n

For n < K * m, the arm pulled at time n is the arm n % K.

theorem Bandits.ETC.arm_mul {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) : A (K * m) =ᵐ[P] fun (ω : Ω) => argmax (Learning.empMean' (K * m) (Learning.history O A R (K * m) ω))

The arm pulled at time K * m is the arm with the highest empirical mean after the exploration phase.

theorem Bandits.ETC.arm_add_one_of_ge {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) {n : ℕ} (hn : K * m ≤ n) : A (n + 1) =ᵐ[P] fun (ω : Ω) => A n ω

For n ≥ K * m, the arm pulled at time n + 1 is the same as the arm pulled at time n.

theorem Bandits.ETC.arm_of_ge {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) {n : ℕ} (hn : K * m ≤ n) : A n =ᵐ[P] A (K * m)

For n ≥ K * m, the arm pulled at time n is the same as the arm pulled at time K * m.

theorem Bandits.ETC.pullCount_mul {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (a : Fin K) : Learning.pullCount A a (K * m) =ᵐ[P] fun (x : Ω) => m

At time K * m, the number of pulls of each arm is equal to m.

theorem Bandits.ETC.pullCount_add_one_of_ge {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (a : Fin K) {n : ℕ} (hn : K * m ≤ n) : Learning.pullCount A a (n + 1) =ᵐ[P] fun (ω : Ω) => Learning.pullCount A a n ω + {ω' : Ω | A (K * m) ω' = a}.indicator 1 ω

theorem Bandits.ETC.pullCount_of_ge {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (a : Fin K) {n : ℕ} (hn : K * m ≤ n) : Learning.pullCount A a n =ᵐ[P] fun (ω : Ω) => m + (n - K * m) * {ω' : Ω | A (K * m) ω' = a}.indicator 1 ω

For n ≥ K * m, the number of pulls of each arm a at time n is equal to m plus n - K * m if arm a is the best arm after the exploration phase.

theorem Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq {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 : ℕ → Ω → ℝ} (h : Learning.IsAlgEnvSeq O A R (etcAlgorithm K m) (Learning.stationaryEnv ν) P) (a : Fin K) (hm : m ≠ 0) : ∀ᵐ (ω : Ω) ∂P, A (K * m) ω = a → Learning.sumRewards A R (bestArm ν) (K * m) ω ≤ Learning.sumRewards A R a (K * m) ω

If at time K * m the algorithm chooses arm a, then the total reward obtained by pulling arm a is at least the total reward obtained by pulling the best arm.