Regret bounds for the UCB algorithm

theorem Bandits.UCB.gap_le_two_mul_ucbWidth {K : ℕ} [NeZero K] {c : ℝ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} {Ω : Type u_1} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} {b : Fin K} (h_best : ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤ Learning.empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω) (h_arm : Learning.empMean A R b n ω - ucbWidth A c b n ω ≤ ∫ (x : ℝ), id x ∂ν b) (h_le : Learning.empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω ≤ Learning.empMean A R b n ω + ucbWidth A c b n ω) : gap ν b ≤ 2 * ucbWidth A c b n ω

If the means of the best arm and of arm b lie in their confidence intervals and the UCB index of b is at least that of the best arm, then the gap of b is at most twice its confidence width.

theorem Bandits.UCB.pullCount_le_of_ucbIndex_le {K : ℕ} [NeZero K] {c : ℝ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} {Ω : Type u_1} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hc : 0 ≤ c) {b : Fin K} (h_best : ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤ Learning.empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω) (h_arm : Learning.empMean A R b n ω - ucbWidth A c b n ω ≤ ∫ (x : ℝ), id x ∂ν b) (h_le : Learning.empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω ≤ Learning.empMean A R b n ω + ucbWidth A c b n ω) (h_gap_pos : 0 < gap ν b) (h_pull_pos : 0 < Learning.pullCount A b n ω) : ↑(Learning.pullCount A b n ω) ≤ 8 * c * Real.log (↑n + 1) / gap ν b ^ 2

If the means of the best arm and of arm b lie in their confidence intervals and the UCB index of b is at least that of the best arm, then the number of pulls of b is at most 8 * c * log (n + 1) / gap ν b ^ 2.

theorem Bandits.UCB.prob_ucbIndex_le {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 : ℕ → Ω → ℝ} {σ2 : NNReal} {alg : Learning.Algorithm Unit (Fin K) ℝ} (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : Fin K) (n : ℕ) : P {ω : Ω | 0 < Learning.pullCount A a n ω ∧ Learning.empMean A R a n ω + ucbWidth A (c * ↑σ2) a n ω ≤ ∫ (x : ℝ), id x ∂ν a} ≤ 1 / (↑n + 1) ^ (c - 1)

The probability that the UCB index of arm a is below its mean is at most 1 / (n + 1) ^ (c - 1).

theorem Bandits.UCB.prob_lcbIndex_ge {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 : ℕ → Ω → ℝ} {σ2 : NNReal} {alg : Learning.Algorithm Unit (Fin K) ℝ} (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : Fin K) (n : ℕ) : P {ω : Ω | 0 < Learning.pullCount A a n ω ∧ ∫ (x : ℝ), id x ∂ν a ≤ Learning.empMean A R a n ω - ucbWidth A (c * ↑σ2) a n ω} ≤ 1 / (↑n + 1) ^ (c - 1)

The probability that the lower confidence bound of arm a is above its mean is at most 1 / (n + 1) ^ (c - 1).

theorem Bandits.UCB.pullCount_le_add_three {K : ℕ} [NeZero K] {c : ℝ} {ν : ProbabilityTheory.Kernel (Fin K) ℝ} {Ω : Type u_1} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} (a : Fin K) (n C : ℕ) (ω : Ω) : Learning.pullCount A a n ω ≤ C + 1 + ∑ s ∈ Finset.range n, {s : ℕ | A s ω = a ∧ C < Learning.pullCount A a s ω ∧ ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤ Learning.empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω ∧ Learning.empMean A R (A s ω) s ω - ucbWidth A c (A s ω) s ω ≤ ∫ (x : ℝ), id x ∂ν (A s ω)}.indicator 1 s + ∑ s ∈ Finset.range n, {s : ℕ | C < Learning.pullCount A a s ω ∧ Learning.empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω < ∫ (x : ℝ), id x ∂ν (bestArm ν)}.indicator 1 s + ∑ s ∈ Finset.range n, {s : ℕ | C < Learning.pullCount A a s ω ∧ ∫ (x : ℝ), id x ∂ν a < Learning.empMean A R a s ω - ucbWidth A c a s ω}.indicator 1 s

theorem Bandits.UCB.pullCount_le_add_three_ae {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) (n C : ℕ) (hC : C ≠ 0) : ∀ᵐ (ω : Ω) ∂P, Learning.pullCount A a n ω ≤ C + 1 + ∑ s ∈ Finset.range n, {s : ℕ | A s ω = a ∧ C < Learning.pullCount A a s ω ∧ ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤ Learning.empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω ∧ Learning.empMean A R (A s ω) s ω - ucbWidth A c (A s ω) s ω ≤ ∫ (x : ℝ), id x ∂ν (A s ω)}.indicator 1 s + ∑ s ∈ Finset.range n, {s : ℕ | 0 < Learning.pullCount A (bestArm ν) s ω ∧ Learning.empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω < ∫ (x : ℝ), id x ∂ν (bestArm ν)}.indicator 1 s + ∑ s ∈ Finset.range n, {s : ℕ | 0 < Learning.pullCount A a s ω ∧ ∫ (x : ℝ), id x ∂ν a < Learning.empMean A R a s ω - ucbWidth A c a s ω}.indicator 1 s

theorem Bandits.UCB.sum_indicator_good_event_eq_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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K (c * ↑σ2)) (Learning.stationaryEnv ν) P) (hc : 0 ≤ c) (a : Fin K) (h_gap : 0 < gap ν a) (n C : ℕ) (hC : C ≠ 0) (hC' : 8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a ^ 2 ≤ ↑C) : ∀ᵐ (ω : Ω) ∂P, ∑ s ∈ Finset.range n, {s : ℕ | A s ω = a ∧ C < Learning.pullCount A a s ω ∧ ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤ Learning.empMean A R (bestArm ν) s ω + ucbWidth A (c * ↑σ2) (bestArm ν) s ω ∧ Learning.empMean A R (A s ω) s ω - ucbWidth A (c * ↑σ2) (A s ω) s ω ≤ ∫ (x : ℝ), id x ∂ν (A s ω)}.indicator 1 s = 0

If C ≥ 8 * c * σ2 * log (n + 1) / gap ν a ^ 2, then arm a is never pulled at a time s < n at which it already has more than C pulls and the means of the best arm and of a lie in their confidence intervals.

theorem Bandits.UCB.pullCount_ae_le_add_two {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K (c * ↑σ2)) (Learning.stationaryEnv ν) P) (hc : 0 ≤ c) (a : Fin K) (h_gap : 0 < gap ν a) (n C : ℕ) (hC : C ≠ 0) (hC' : 8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a ^ 2 ≤ ↑C) : ∀ᵐ (ω : Ω) ∂P, Learning.pullCount A a n ω ≤ C + 1 + ∑ s ∈ Finset.range n, {s : ℕ | 0 < Learning.pullCount A (bestArm ν) s ω ∧ Learning.empMean A R (bestArm ν) s ω + ucbWidth A (c * ↑σ2) (bestArm ν) s ω < ∫ (x : ℝ), id x ∂ν (bestArm ν)}.indicator 1 s + ∑ s ∈ Finset.range n, {s : ℕ | 0 < Learning.pullCount A a s ω ∧ ∫ (x : ℝ), id x ∂ν a < Learning.empMean A R a s ω - ucbWidth A (c * ↑σ2) a s ω}.indicator 1 s

noncomputable def Bandits.UCB.constSum (c : ℝ) (n : ℕ) : ℝ

A sum that appears in the UCB regret upper bound. For c > 2 it is bounded uniformly in n, see constSum_le.

Equations

• Bandits.UCB.constSum c n = ∑ s ∈ Finset.range n, 1 / (↑s + 1) ^ (c - 1)

theorem Bandits.UCB.constSum_nonneg (c : ℝ) (n : ℕ) : 0 ≤ constSum c n

theorem Bandits.UCB.ofReal_constSum (c : ℝ) (n : ℕ) : ENNReal.ofReal (constSum c n) = ∑ s ∈ Finset.range n, 1 / (↑s + 1) ^ (c - 1)

theorem Bandits.UCB.constSum_le {c : ℝ} (hc : 2 < c) (n : ℕ) : constSum c n ≤ 1 + 1 / (c - 2)

For c > 2, the sum constSum c n is at most 1 + 1 / (c - 2), uniformly in n.

theorem Bandits.UCB.expectation_pullCount_le' {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K (c * ↑σ2)) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) : ∫⁻ (ω : Ω), ↑(Learning.pullCount A a n ω) ∂P ≤ ENNReal.ofReal (8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a ^ 2 + 1) + 1 + 2 * ENNReal.ofReal (constSum c n)

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

theorem Bandits.UCB.expectation_pullCount_le {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K (c * ↑σ2)) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) : ∫ (x : Ω), (fun (ω : Ω) => ↑(Learning.pullCount A a n ω)) x ∂P ≤ 8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a ^ 2 + 2 + 2 * constSum c n

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

theorem Bandits.UCB.regret_le {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K (c * ↑σ2)) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) : ∫ (x : Ω), regret ν A n x ∂P ≤ ∑ a : Fin K, (8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a + gap ν a * (2 + 2 * constSum c n))

Regret bound for the UCB algorithm.

theorem Bandits.UCB.regret_le_of_gt_two {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K (c * ↑σ2)) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 2 < c) (n : ℕ) : ∫ (x : Ω), regret ν A n x ∂P ≤ ∑ a : Fin K, (8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a + gap ν a * (4 + 2 / (c - 2)))

Regret bound for the UCB algorithm with an explicit constant, for c > 2.

theorem Bandits.UCB.regret_le' {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) : ∫ (x : Ω), regret ν A n x ∂P ≤ ∑ a : Fin K, (8 * c * Real.log (↑n + 1) / gap ν a + gap ν a * (2 + 2 * constSum (c / ↑σ2) n))

Regret bound for the UCB algorithm with exploration constant c, for σ2-subgaussian rewards.

theorem Bandits.UCB.regret_le_of_gt_two' {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 : ℕ → Ω → ℝ} {σ2 : NNReal} (h : Learning.IsAlgEnvSeq O A R (ucbAlgorithm K c) (Learning.stationaryEnv ν) P) (hν : ∀ (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun (x : ℝ) => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 2 * ↑σ2 < c) (n : ℕ) : ∫ (x : Ω), regret ν A n x ∂P ≤ ∑ a : Fin K, (8 * c * Real.log (↑n + 1) / gap ν a + gap ν a * (4 + 2 * ↑σ2 / (c - 2 * ↑σ2)))

Regret bound for the UCB algorithm with exploration constant c > 2 * σ2, for σ2-subgaussian rewards, with an explicit constant.