Skip to content

Generalize ETC and UCB regret bounds #64

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 3 commits into from
Jan 21, 2026
Merged

Generalize ETC and UCB regret bounds #64

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2ff66d8
change parametrization of ucb
RemyDegenne Jan 21, 2026
b5a7e2f
generalize from 1 to sigma2 subgaussian
RemyDegenne Jan 21, 2026
9f28009
minor
RemyDegenne Jan 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 27 additions & 31 deletions LeanBandits/Bandit/SumRewards.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -517,14 +517,14 @@ lemma probReal_sumRewards_le_sumRewards_le [Fintype α] (h : IsAlgEnvSeq A R alg
section Subgaussian

omit [DecidableEq α] [StandardBorelSpace α] in
lemma probReal_sum_le_sum_streamMeasure [Fintype α]
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (a : α) (m : ℕ) :
lemma probReal_sum_le_sum_streamMeasure [Fintype α] {c : ℝ≥0}
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (a : α) (m : ℕ) :
(streamMeasure ν).real
{ω | ∑ s ∈ range m, ω s (bestArm ν) ≤ ∑ s ∈ range m, ω s a} ≤
Real.exp (-↑m * gap ν a ^ 2 / 4) := by
Real.exp (-↑m * gap ν a ^ 2 / (4 * c)) := by
by_cases ha : a = bestArm ν
· simp [ha]
refine (HasSubgaussianMGF.measure_sum_le_sum_le' (cX := fun _ ↦ 1) (cY := fun _ ↦ 1)
refine (HasSubgaussianMGF.measure_sum_le_sum_le' (cX := fun _ ↦ c) (cY := fun _ ↦ c)
?_ ?_ ?_ ?_ ?_ ?_).trans_eq ?_
· exact iIndepFun_eval_streamMeasure'' ν (bestArm ν)
· exact iIndepFun_eval_streamMeasure'' ν a
Expand All @@ -542,70 +542,66 @@ lemma probReal_sum_le_sum_streamMeasure [Fintype α]
exact le_bestArm a
· congr 1
simp_rw [integral_eval_streamMeasure]
simp only [id_eq, sum_const, card_range, nsmul_eq_mul, mul_one, NNReal.coe_natCast,
simp only [id_eq, sum_const, card_range, nsmul_eq_mul, NNReal.coe_mul, NNReal.coe_natCast,
gap_eq_bestArm_sub, neg_mul]
field_simp
ring

omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in
lemma prob_sum_le_sqrt_log
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) {c : ℝ} (hc : 0 ≤ c)
(a : α) (k : ℕ) (hk : k ≠ 0) :
lemma prob_sum_le_sqrt_log {σ2 : ℝ≥0}
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
(hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : α) (k : ℕ) (hk : k ≠ 0) :
streamMeasure ν
{ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(c * k * Real.log (n + 1))} ≤
1 / (n + 1) ^ (c / 2) := by
{ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * Real.log (n + 1))} ≤
1 / (n + 1) ^ c := by
calc
streamMeasure ν
{ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(c * k * Real.log (n + 1))}
_ ≤ ENNReal.ofReal (Real.exp (-(√(c * k * Real.log (n + 1))) ^ 2 / (2 * k * 1))) := by
{ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * Real.log (n + 1))}
_ ≤ ENNReal.ofReal (Real.exp (-(√(2 * c * k * σ2 * Real.log (n + 1))) ^ 2 / (2 * k * σ2))) := by
rw [← ofReal_measureReal]
gcongr
refine (HasSubgaussianMGF.measure_sum_range_le_le_of_iIndepFun (c := 1) ?_ ?_ (by positivity))
refine (HasSubgaussianMGF.measure_sum_range_le_le_of_iIndepFun (c := σ2) ?_ ?_ (by positivity))
· exact (iIndepFun_eval_streamMeasure'' ν a).comp (fun i ω ↦ ω - (ν a)[id])
(fun _ ↦ by fun_prop)
· intro i him
refine (hν a).congr_identDistrib ?_
exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
_ = 1 / (n + 1) ^ (c / 2) := by
_ = 1 / (n + 1) ^ c := by
rw [Real.sq_sqrt]
swap; · exact mul_nonneg (by positivity) (Real.log_nonneg (by simp))
field_simp
rw [div_eq_inv_mul, ← mul_assoc, ← Real.log_rpow (by positivity), ← Real.log_inv,
rw [← Real.log_rpow (by positivity), ← Real.log_inv,
Real.exp_log (by positivity), one_div, ENNReal.ofReal_inv_of_pos (by positivity),
← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
congr 2
· norm_cast
· field
norm_cast

omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in
lemma prob_sum_ge_sqrt_log
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) {c : ℝ} (hc : 0 ≤ c)
(a : α) (k : ℕ) (hk : k ≠ 0) :
lemma prob_sum_ge_sqrt_log {σ2 : ℝ≥0}
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
(hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : α) (k : ℕ) (hk : k ≠ 0) :
streamMeasure ν
{ω | √(c * k * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} ≤
1 / (n + 1) ^ (c / 2) := by
{ω | √(2 * c * k * σ2 * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} ≤
1 / (n + 1) ^ c := by
calc
streamMeasure ν
{ω | √(c * k * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))}
_ ≤ ENNReal.ofReal (Real.exp (-(√(c * k * Real.log (n + 1))) ^ 2 / (2 * k * 1))) := by
{ω | √(2 * c * k * σ2 * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))}
_ ≤ ENNReal.ofReal (Real.exp (-(√(2 * c * k * σ2 * Real.log (n + 1))) ^ 2 / (2 * k * σ2))) := by
rw [← ofReal_measureReal]
gcongr
refine (HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun (c := 1) ?_ ?_ (by positivity))
refine (HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun (c := σ2) ?_ ?_ (by positivity))
· exact (iIndepFun_eval_streamMeasure'' ν a).comp (fun i ω ↦ ω - (ν a)[id])
(fun _ ↦ by fun_prop)
· intro i him
refine (hν a).congr_identDistrib ?_
exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
_ = 1 / (n + 1) ^ (c / 2) := by
_ = 1 / (n + 1) ^ c := by
rw [Real.sq_sqrt]
swap; · exact mul_nonneg (by positivity) (Real.log_nonneg (by simp))
field_simp
rw [div_eq_inv_mul, ← mul_assoc, ← Real.log_rpow (by positivity), ← Real.log_inv,
rw [← Real.log_rpow (by positivity), ← Real.log_inv,
Real.exp_log (by positivity), one_div, ENNReal.ofReal_inv_of_pos (by positivity),
← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
congr 2
· norm_cast
· field
norm_cast

end Subgaussian

Expand Down
17 changes: 9 additions & 8 deletions LeanBandits/BanditAlgorithms/ETC.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ variable {hK : 0 < K} {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
{Ω : Type*} {mΩ : MeasurableSpace Ω}
{P : Measure Ω} [IsProbabilityMeasure P]
{A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
{σ2 : ℝ≥0}

lemma arm_zero [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
Expand Down Expand Up @@ -194,9 +195,9 @@ lemma sumRewards_bestArm_le_of_arm_mul_eq [Nonempty (Fin K)]

lemma probReal_sumRewards_le_sumRewards_le [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (a : Fin K) :
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K) :
P.real {ω | sumRewards A R (bestArm ν) (K * m) ω ≤ sumRewards A R a (K * m) ω} ≤
Real.exp (-↑m * gap ν a ^ 2 / 4) := by
Real.exp (-↑m * gap ν a ^ 2 / (4 * σ2)) := by
have hA := h.measurable_A
have hR := h.measurable_R
have h1 := Bandits.probReal_sumRewards_le_sumRewards_le h a (K * m) m m
Expand All @@ -213,9 +214,9 @@ lemma probReal_sumRewards_le_sumRewards_le [Nonempty (Fin K)]
`exp(- m * Δ_a^2 / 4)`. -/
lemma prob_arm_mul_eq_le [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (a : Fin K)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K)
(hm : m ≠ 0) :
P.real {ω | A (K * m) ω = a} ≤ Real.exp (- (m : ℝ) * gap ν a ^ 2 / 4) := by
P.real {ω | A (K * m) ω = a} ≤ Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2)) := by
have h_pos : 0 < K * m := Nat.mul_pos hK hm.bot_lt
have h_le : P.real {ω | A (K * m) ω = a}
≤ P.real {ω | sumRewards A R (bestArm ν) (K * m) ω ≤ sumRewards A R a (K * m) ω} := by
Expand All @@ -229,10 +230,10 @@ lemma prob_arm_mul_eq_le [Nonempty (Fin K)]
/-- Bound on the expectation of the number of pulls of each arm by the ETC algorithm. -/
lemma expectation_pullCount_le [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a))
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
(a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
P[fun ω ↦ (pullCount A a n ω : ℝ)]
≤ m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / 4) := by
≤ m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2)) := by
have hA := h.measurable_A
have hR := h.measurable_R
have : (fun ω ↦ (pullCount A a n ω : ℝ))
Expand All @@ -259,10 +260,10 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
/-- Regret bound for the ETC algorithm. -/
lemma regret_le [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (hm : m ≠ 0)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hm : m ≠ 0)
(n : ℕ) (hn : K * m ≤ n) :
P[regret ν A n] ≤
∑ a, gap ν a * (m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / 4)) := by
∑ a, gap ν a * (m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2))) := by
have hA := h.measurable_A
simp_rw [regret_eq_sum_pullCount_mul_gap]
rw [integral_finset_sum]
Expand Down
Loading