From 5769035d9c91f45e7e4935f5932f0a8fe6738fbd Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 6 Jan 2026 11:35:39 +0000 Subject: [PATCH 1/8] Basic properties relating regret and gaps --- LeanBandits/Bandit/Regret.lean | 33 ++++++++++++++++++++++++++------- 1 file changed, 26 insertions(+), 7 deletions(-) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index acabf6c8..63bf1786 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -20,12 +20,7 @@ namespace Bandits variable {α : Type*} [DecidableEq α] {mα : MeasurableSpace α} {ν : Kernel α ℝ} {h : ℕ → α × ℝ} {m n t : ℕ} {a : α} -/-! ### Definitions of regret, gaps, pull counts -/ - -/-- Regret of a sequence of pulls `k : ℕ → α` at time `t` for the reward kernel `ν ; Kernel α ℝ`. -/ -noncomputable -def regret (ν : Kernel α ℝ) (t : ℕ) (h : ℕ → α × ℝ) : ℝ := - t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (arm s h))[id] +/-! ### Definitions of gaps, regret, pull counts -/ /-- Gap of an arm `a`: difference between the highest mean of the arms and the mean of `a`. -/ noncomputable @@ -36,6 +31,26 @@ lemma gap_nonneg [Fintype α] : 0 ≤ gap ν a := by rw [gap, sub_nonneg] exact le_ciSup (f := fun i ↦ (ν i)[id]) (by simp) a +/-- Regret of a sequence of pulls `k : ℕ → α` at time `t` for the reward kernel `ν ; Kernel α ℝ`. -/ +noncomputable +def regret (ν : Kernel α ℝ) (t : ℕ) (h : ℕ → α × ℝ) : ℝ := + t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (arm s h))[id] + +omit [DecidableEq α] in +lemma regret_eq_sum_gap : regret ν t h = ∑ s ∈ range t, gap ν (arm s h) := by + simp [regret, gap] + +omit [DecidableEq α] in +lemma regret_nonneg [Fintype α] : 0 ≤ regret ν t h := by + rw [regret_eq_sum_gap] + exact sum_nonneg (fun _ _ ↦ gap_nonneg) + +omit [DecidableEq α] in +lemma gap_eq_zero_of_regret_eq_zero [Fintype α] (hr : regret ν t h = 0) {s : ℕ} (hs : s < t) : + gap ν (arm s h) = 0 := by + rw [regret_eq_sum_gap] at hr + exact (sum_eq_zero_iff_of_nonneg fun _ _ ↦ gap_nonneg).1 hr s (mem_range.2 hs) + lemma arm_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount a (s + 1) h = m) : arm (stepsUntil a m h).toNat h = a := by exact action_stepsUntil hm h_exists @@ -49,7 +64,7 @@ section RewardByCount lemma regret_eq_sum_pullCount_mul_gap [Fintype α] : regret ν t h = ∑ a, pullCount a t h * gap ν a := by - simp [sum_pullCount_mul, regret, gap, sum_sub_distrib, arm, action] + simp_rw [regret_eq_sum_gap, arm, sum_pullCount_mul, action] end RewardByCount @@ -73,6 +88,10 @@ lemma gap_eq_bestArm_sub : gap ν a = (ν (bestArm ν))[id] - (ν a)[id] := by refine le_antisymm ?_ (le_ciSup (f := fun a ↦ (ν a)[id]) (by simp) (bestArm ν)) exact ciSup_le le_bestArm +omit [DecidableEq α] in +lemma integral_id_eq_of_gap_eq_zero (h : gap ν a = 0) : (ν a)[id] = (ν (bestArm ν))[id] := + (sub_eq_zero.1 (gap_eq_bestArm_sub (a := a) ▸ h)).symm + omit [DecidableEq α] in @[simp] lemma gap_bestArm : gap ν (bestArm ν) = 0 := by From dcf4d7b43d627f2d5efedf33003721d6ba6ba6b4 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 6 Jan 2026 11:51:35 +0000 Subject: [PATCH 2/8] Minor clarification --- LeanBandits/Bandit/Regret.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index 63bf1786..dc647968 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -64,7 +64,7 @@ section RewardByCount lemma regret_eq_sum_pullCount_mul_gap [Fintype α] : regret ν t h = ∑ a, pullCount a t h * gap ν a := by - simp_rw [regret_eq_sum_gap, arm, sum_pullCount_mul, action] + simp_rw [regret_eq_sum_gap, sum_pullCount_mul, arm, action] end RewardByCount @@ -89,8 +89,9 @@ lemma gap_eq_bestArm_sub : gap ν a = (ν (bestArm ν))[id] - (ν a)[id] := by exact ciSup_le le_bestArm omit [DecidableEq α] in -lemma integral_id_eq_of_gap_eq_zero (h : gap ν a = 0) : (ν a)[id] = (ν (bestArm ν))[id] := - (sub_eq_zero.1 (gap_eq_bestArm_sub (a := a) ▸ h)).symm +lemma integral_id_eq_of_gap_eq_zero (hg : gap ν a = 0) : (ν a)[id] = (ν (bestArm ν))[id] := by + rw [gap_eq_bestArm_sub, sub_eq_zero] at hg + exact hg.symm omit [DecidableEq α] in @[simp] From 27311a432aa088cbf60ab88296544f18f28153c3 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 6 Jan 2026 13:08:47 +0000 Subject: [PATCH 3/8] Definition of bestPullCount --- LeanBandits/Bandit/Regret.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index dc647968..b6552351 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -98,6 +98,16 @@ omit [DecidableEq α] in lemma gap_bestArm : gap ν (bestArm ν) = 0 := by rw [gap_eq_bestArm_sub, sub_self] +/-- Number of times an optimal arm was chosen up to time `t` (excluding `t`). -/ +noncomputable +def bestPullCount (ν : Kernel α ℝ) (t : ℕ) (h : ℕ → α × ℝ) : ℕ := + #(filter (fun s ↦ gap ν (arm s h) = 0) (range t)) + +omit [DecidableEq α] [Nonempty α] in +lemma bestPullCount_eq_of_regret_eq_zero (hr : regret ν t h = 0) : bestPullCount ν t h = t := by + rw [bestPullCount, filter_true_of_mem, card_range] + exact fun s hs ↦ gap_eq_zero_of_regret_eq_zero hr (mem_range.1 hs) + end BestArm end Bandits From a945acf92ff464f47f731db1c887de0eed84da33 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 6 Jan 2026 14:13:52 +0000 Subject: [PATCH 4/8] Sublinear regret implies average reward becoming highest mean --- LeanBandits/Bandit/Regret.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index b6552351..4a129479 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -110,4 +110,21 @@ lemma bestPullCount_eq_of_regret_eq_zero (hr : regret ν t h = 0) : bestPullCoun end BestArm +section Asymptotics + +omit [DecidableEq α] in +lemma tendsto_highest_mean_of_sublinear_regret (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) : + Tendsto (fun t ↦ (∑ s ∈ range t, (ν (arm s h))[id]) / (t : ℝ)) + atTop (nhds (⨆ a, (ν a)[id])) := by + have ht : Tendsto (fun t ↦ (⨆ a, (ν a)[id]) - regret ν t h / t) + atTop (nhds (⨆ a, (ν a)[id])) := by + simpa using (tendsto_const_nhds.sub hr.tendsto_div_nhds_zero) + apply ht.congr' + filter_upwards [eventually_ne_atTop 0] with t ht + rw [regret] + field_simp + ring + +end Asymptotics + end Bandits From b9b88d336ef3c3666b70fcc6d134c12bd37b2a77 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 6 Jan 2026 15:55:50 +0000 Subject: [PATCH 5/8] PullCount rate of suboptimal arms tends to zero when regret is sublinear --- LeanBandits/Bandit/Regret.lean | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index 4a129479..0a282b5a 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -98,22 +98,13 @@ omit [DecidableEq α] in lemma gap_bestArm : gap ν (bestArm ν) = 0 := by rw [gap_eq_bestArm_sub, sub_self] -/-- Number of times an optimal arm was chosen up to time `t` (excluding `t`). -/ -noncomputable -def bestPullCount (ν : Kernel α ℝ) (t : ℕ) (h : ℕ → α × ℝ) : ℕ := - #(filter (fun s ↦ gap ν (arm s h) = 0) (range t)) - -omit [DecidableEq α] [Nonempty α] in -lemma bestPullCount_eq_of_regret_eq_zero (hr : regret ν t h = 0) : bestPullCount ν t h = t := by - rw [bestPullCount, filter_true_of_mem, card_range] - exact fun s hs ↦ gap_eq_zero_of_regret_eq_zero hr (mem_range.1 hs) - end BestArm section Asymptotics omit [DecidableEq α] in -lemma tendsto_highest_mean_of_sublinear_regret (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) : +lemma avg_mean_reward_tendsto_highest_mean_of_sublinear_regret + (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) : Tendsto (fun t ↦ (∑ s ∈ range t, (ν (arm s h))[id]) / (t : ℝ)) atTop (nhds (⨆ a, (ν a)[id])) := by have ht : Tendsto (fun t ↦ (⨆ a, (ν a)[id]) - regret ν t h / t) @@ -125,6 +116,20 @@ lemma tendsto_highest_mean_of_sublinear_regret (hr : (regret ν · h) =o[atTop] field_simp ring +lemma pullCount_rate_tendsto_zero_of_sublinear_regret [Fintype α] + (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) (hg : gap ν a ≠ 0) : + Tendsto (fun t ↦ (pullCount a t h : ℝ) / t) atTop (nhds 0) := by + have hb : ∀ᶠ t in atTop, (pullCount a t h : ℝ) / t ≤ regret ν t h / t / gap ν a := by + filter_upwards [eventually_gt_atTop 0] with t ht + have ht' : (0 : ℝ) < t := Nat.cast_pos.mpr ht + rw [le_div_iff₀ (gap_nonneg.lt_of_ne' hg), div_mul_eq_mul_div, le_div_iff₀ ht', + div_mul_cancel₀ _ ht'.ne'] + rw [regret_eq_sum_pullCount_mul_gap] + exact single_le_sum (f := fun b ↦ (pullCount b t h : ℝ) * gap ν b) + (fun _ _ ↦ mul_nonneg (Nat.cast_nonneg _) gap_nonneg) (mem_univ a) + exact squeeze_zero' (Eventually.of_forall fun _ ↦ by positivity) + hb (by simpa using hr.tendsto_div_nhds_zero.div_const (gap ν a)) + end Asymptotics end Bandits From 94b33cec6ca8dcd5408cdd93c464bbd9644dfabe Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Wed, 7 Jan 2026 11:09:05 +0000 Subject: [PATCH 6/8] Minor changes --- LeanBandits/Bandit/Regret.lean | 36 ++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index 0a282b5a..5bd16e84 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -31,7 +31,7 @@ lemma gap_nonneg [Fintype α] : 0 ≤ gap ν a := by rw [gap, sub_nonneg] exact le_ciSup (f := fun i ↦ (ν i)[id]) (by simp) a -/-- Regret of a sequence of pulls `k : ℕ → α` at time `t` for the reward kernel `ν ; Kernel α ℝ`. -/ +/-- Regret of a history `h` at time `t` for the reward kernel `ν : Kernel α ℝ`. -/ noncomputable def regret (ν : Kernel α ℝ) (t : ℕ) (h : ℕ → α × ℝ) : ℝ := t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (arm s h))[id] @@ -89,7 +89,7 @@ lemma gap_eq_bestArm_sub : gap ν a = (ν (bestArm ν))[id] - (ν a)[id] := by exact ciSup_le le_bestArm omit [DecidableEq α] in -lemma integral_id_eq_of_gap_eq_zero (hg : gap ν a = 0) : (ν a)[id] = (ν (bestArm ν))[id] := by +lemma integral_eq_of_gap_eq_zero (hg : gap ν a = 0) : (ν a)[id] = (ν (bestArm ν))[id] := by rw [gap_eq_bestArm_sub, sub_eq_zero] at hg exact hg.symm @@ -103,32 +103,34 @@ end BestArm section Asymptotics omit [DecidableEq α] in -lemma avg_mean_reward_tendsto_highest_mean_of_sublinear_regret - (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) : +lemma avg_mean_reward_tendsto_of_sublinear_regret (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) : Tendsto (fun t ↦ (∑ s ∈ range t, (ν (arm s h))[id]) / (t : ℝ)) atTop (nhds (⨆ a, (ν a)[id])) := by have ht : Tendsto (fun t ↦ (⨆ a, (ν a)[id]) - regret ν t h / t) atTop (nhds (⨆ a, (ν a)[id])) := by - simpa using (tendsto_const_nhds.sub hr.tendsto_div_nhds_zero) + simpa using tendsto_const_nhds.sub hr.tendsto_div_nhds_zero apply ht.congr' filter_upwards [eventually_ne_atTop 0] with t ht rw [regret] field_simp ring -lemma pullCount_rate_tendsto_zero_of_sublinear_regret [Fintype α] - (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) (hg : gap ν a ≠ 0) : +lemma pullCount_rate_tendsto_of_sublinear_regret [Fintype α] + (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) (hg : 0 < gap ν a) : Tendsto (fun t ↦ (pullCount a t h : ℝ) / t) atTop (nhds 0) := by - have hb : ∀ᶠ t in atTop, (pullCount a t h : ℝ) / t ≤ regret ν t h / t / gap ν a := by - filter_upwards [eventually_gt_atTop 0] with t ht - have ht' : (0 : ℝ) < t := Nat.cast_pos.mpr ht - rw [le_div_iff₀ (gap_nonneg.lt_of_ne' hg), div_mul_eq_mul_div, le_div_iff₀ ht', - div_mul_cancel₀ _ ht'.ne'] - rw [regret_eq_sum_pullCount_mul_gap] - exact single_le_sum (f := fun b ↦ (pullCount b t h : ℝ) * gap ν b) - (fun _ _ ↦ mul_nonneg (Nat.cast_nonneg _) gap_nonneg) (mem_univ a) - exact squeeze_zero' (Eventually.of_forall fun _ ↦ by positivity) - hb (by simpa using hr.tendsto_div_nhds_zero.div_const (gap ν a)) + have hb (t : ℕ) : (pullCount a t h : ℝ) / t ≤ regret ν t h / t / gap ν a := by + obtain ht | ht := eq_or_ne t 0 + · simp [ht] + · calc (pullCount a t h : ℝ) / t + = pullCount a t h * gap ν a / gap ν a / t := by field_simp + _ ≤ regret ν t h / gap ν a / t := by + gcongr + rw [regret_eq_sum_pullCount_mul_gap] + exact single_le_sum (f := fun a ↦ (pullCount a t h : ℝ) * gap ν a) + (fun _ _ ↦ mul_nonneg (Nat.cast_nonneg _) gap_nonneg) (mem_univ a) + _ = regret ν t h / t / gap ν a := by ring + apply squeeze_zero' (Eventually.of_forall fun _ ↦ by positivity) (Eventually.of_forall hb) + simpa using hr.tendsto_div_nhds_zero.div_const (gap ν a) end Asymptotics From 7100c4dba064a0391452a8e370e1153e71f01aea Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Wed, 7 Jan 2026 11:56:25 +0000 Subject: [PATCH 7/8] Improved clarity --- LeanBandits/Bandit/Regret.lean | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index 5bd16e84..9a3bc426 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -89,9 +89,8 @@ lemma gap_eq_bestArm_sub : gap ν a = (ν (bestArm ν))[id] - (ν a)[id] := by exact ciSup_le le_bestArm omit [DecidableEq α] in -lemma integral_eq_of_gap_eq_zero (hg : gap ν a = 0) : (ν a)[id] = (ν (bestArm ν))[id] := by - rw [gap_eq_bestArm_sub, sub_eq_zero] at hg - exact hg.symm +lemma integral_eq_of_gap_eq_zero (hg : gap ν a = 0) : (ν (bestArm ν))[id] = (ν a)[id] := by + rwa [← sub_eq_zero, ← gap_eq_bestArm_sub] omit [DecidableEq α] in @[simp] @@ -118,18 +117,18 @@ lemma avg_mean_reward_tendsto_of_sublinear_regret (hr : (regret ν · h) =o[atTo lemma pullCount_rate_tendsto_of_sublinear_regret [Fintype α] (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) (hg : 0 < gap ν a) : Tendsto (fun t ↦ (pullCount a t h : ℝ) / t) atTop (nhds 0) := by - have hb (t : ℕ) : (pullCount a t h : ℝ) / t ≤ regret ν t h / t / gap ν a := by + have hb (t : ℕ) : (pullCount a t h : ℝ) * gap ν a ≤ regret ν t h := by + rw [regret_eq_sum_pullCount_mul_gap] + exact single_le_sum (f := fun a ↦ pullCount a t h * gap ν a) + (fun _ _ ↦ mul_nonneg (Nat.cast_nonneg _) gap_nonneg) (mem_univ a) + have hb' (t : ℕ) : (pullCount a t h : ℝ) / t ≤ regret ν t h / t / gap ν a := by obtain ht | ht := eq_or_ne t 0 · simp [ht] · calc (pullCount a t h : ℝ) / t = pullCount a t h * gap ν a / gap ν a / t := by field_simp - _ ≤ regret ν t h / gap ν a / t := by - gcongr - rw [regret_eq_sum_pullCount_mul_gap] - exact single_le_sum (f := fun a ↦ (pullCount a t h : ℝ) * gap ν a) - (fun _ _ ↦ mul_nonneg (Nat.cast_nonneg _) gap_nonneg) (mem_univ a) + _ ≤ regret ν t h / gap ν a / t := by gcongr; exact hb t _ = regret ν t h / t / gap ν a := by ring - apply squeeze_zero' (Eventually.of_forall fun _ ↦ by positivity) (Eventually.of_forall hb) + apply squeeze_zero' (Eventually.of_forall fun _ ↦ by positivity) (Eventually.of_forall hb') simpa using hr.tendsto_div_nhds_zero.div_const (gap ν a) end Asymptotics From 2406e5c5b8c66d5998e3a8d6a89c68fdf4fa845e Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Wed, 7 Jan 2026 12:16:08 +0000 Subject: [PATCH 8/8] Add comments --- LeanBandits/Bandit/Regret.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean index 9a3bc426..cb878bf6 100644 --- a/LeanBandits/Bandit/Regret.lean +++ b/LeanBandits/Bandit/Regret.lean @@ -102,6 +102,7 @@ end BestArm section Asymptotics omit [DecidableEq α] in +/-- If the regret is sublinear, the average mean reward tends to the highest mean of the arms. -/ lemma avg_mean_reward_tendsto_of_sublinear_regret (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) : Tendsto (fun t ↦ (∑ s ∈ range t, (ν (arm s h))[id]) / (t : ℝ)) atTop (nhds (⨆ a, (ν a)[id])) := by @@ -114,6 +115,7 @@ lemma avg_mean_reward_tendsto_of_sublinear_regret (hr : (regret ν · h) =o[atTo field_simp ring +/-- If the regret is sublinear, the rate of suboptimal arm pulls tends to zero. -/ lemma pullCount_rate_tendsto_of_sublinear_regret [Fintype α] (hr : (regret ν · h) =o[atTop] fun t ↦ (t : ℝ)) (hg : 0 < gap ν a) : Tendsto (fun t ↦ (pullCount a t h : ℝ) / t) atTop (nhds 0) := by