UCB algorithm

noncomputable def Bandits.UCB.ucbWidth' {K : ℕ} (c : ℝ) (n : ℕ) (h : Learning.Hist Unit (Fin K) ℝ n) (a : Fin K) : ℝ

The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval.

Equations

• Bandits.UCB.ucbWidth' c n h a = √(2 * c * Real.log (↑n + 1) / ↑(Learning.pullCount' n h a))

theorem Bandits.UCB.measurable_ucbWidth' {K : ℕ} (c : ℝ) (n : ℕ) (a : Fin K) : Measurable fun (h : Learning.Hist Unit (Fin K) ℝ n) => ucbWidth' c n h a

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

Arm pulled by the UCB algorithm at time n, as a function of the history before n.

Equations

• Bandits.UCB.nextArm K c n h = if n < K then Learning.RoundRobin.nextAction K n else argmax fun (a : Fin K) => Learning.empMean' n h a + Bandits.UCB.ucbWidth' c n h a

theorem Bandits.UCB.measurable_nextArm {K : ℕ} [NeZero K] (c : ℝ) (n : ℕ) : Measurable (nextArm K c n)

The next-arm function of UCB is measurable.

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

The UCB algorithm.

Equations

• Bandits.ucbAlgorithm K c = Learning.detAlgorithm (fun (n : ℕ) (p : Learning.Hist Unit (Fin K) ℝ n × Unit) => Bandits.UCB.nextArm K c n p.1) ⋯

theorem Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) : Learning.IsAlgEnvSeqUntil O A R (Learning.roundRobinAlgorithm K) (Learning.stationaryEnv ν) P K

Before round K, the UCB algorithm behaves like the Round-Robin algorithm.

noncomputable def Bandits.UCB.ucbWidth {K : ℕ} {Ω : Type u_1} (A : ℕ → Ω → Fin K) (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ

The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval.

Equations

• Bandits.UCB.ucbWidth A c a n ω = √(2 * c * Real.log (↑n + 1) / ↑(Learning.pullCount A a n ω))

theorem Bandits.UCB.measurable_ucbWidth {K : ℕ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → Fin K} {n : ℕ} (hA : ∀ (n : ℕ), Measurable (A n)) (c : ℝ) (a : Fin K) : Measurable (ucbWidth A c a n)

theorem Bandits.UCB.ucbWidth_eq_ucbWidth' {K : ℕ} {Ω : Type u_1} {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ucbWidth A c a n ω = ucbWidth' c n (Learning.history O A R n ω) a

theorem Bandits.UCB.arm_zero {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) : A 0 =ᵐ[P] fun (x : Ω) => 0

theorem Bandits.UCB.arm_ae_eq_nextArm {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (n : ℕ) : A n =ᵐ[P] fun (ω : Ω) => nextArm K c n (Learning.history O A R n ω)

theorem Bandits.UCB.ucbIndex_le_ucbIndex_arm {K : ℕ} [NeZero K] {c : ℝ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {n : ℕ} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (a : Fin K) (hn : K ≤ n) : ∀ᵐ (ω : Ω) ∂P, Learning.empMean A R a n ω + ucbWidth A c a n ω ≤ Learning.empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω

theorem Bandits.UCB.forall_arm_eq_mod_of_lt {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) : ∀ᵐ (ω : Ω) ∂P, ∀ n < K, A n ω = Learning.RoundRobin.nextAction K n

theorem Bandits.UCB.forall_ucbIndex_le_ucbIndex_arm {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (a : Fin K) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), K ≤ n → Learning.empMean A R a n ω + ucbWidth A c a n ω ≤ Learning.empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω

theorem Bandits.UCB.time_gt_of_pullCount_gt_one {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (a : Fin K) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), 1 < Learning.pullCount A a n ω → K < n

theorem Bandits.UCB.pullCount_pos_of_pullCount_gt_one {K : ℕ} [NeZero K] {c : ℝ} {ν : 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 (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (a : Fin K) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), 1 < Learning.pullCount A a n ω → ∀ (b : Fin K), 0 < Learning.pullCount A b n ω