Refactor: use several Bandit models

LeanBandits.lean

@@ -1,17 +1,24 @@
 import LeanBandits.Bandit.Bandit
 import LeanBandits.Bandit.Regret
+import LeanBandits.Bandit.RewardByCountMeasure
+import LeanBandits.Bandit.SumRewards
+import LeanBandits.BanditAlgorithms.AuxSums
 import LeanBandits.BanditAlgorithms.ETC
 import LeanBandits.BanditAlgorithms.UCB
 import LeanBandits.ForMathlib.CondDistrib
+import LeanBandits.ForMathlib.CondIndepFun
+import LeanBandits.ForMathlib.HasCondDistrib
 import LeanBandits.ForMathlib.IndepFun
 import LeanBandits.ForMathlib.IndepInfinitePi
+import LeanBandits.ForMathlib.KernelRepresentation
 import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.MeasurableArgMax
+import LeanBandits.ForMathlib.StandardBorel
 import LeanBandits.ForMathlib.SubGaussian
 import LeanBandits.ForMathlib.Traj
-import LeanBandits.RewardByCountMeasure
 import LeanBandits.SequentialLearning.Algorithm
 import LeanBandits.SequentialLearning.Deterministic
 import LeanBandits.SequentialLearning.FiniteActions
+import LeanBandits.SequentialLearning.IonescuTulceaSpace
 import LeanBandits.SequentialLearning.StationaryEnv

LeanBandits/Bandit/Regret.lean

@@ -3,11 +3,10 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Paulo Rauber
 -/
-import LeanBandits.Bandit.Bandit
 import LeanBandits.SequentialLearning.FiniteActions
 
 /-!
-# Regret
+# Regret, gap, best arm
 
 -/
 
@@ -17,17 +16,12 @@ open scoped ENNReal NNReal
 
 namespace Bandits
 
-variable {α : Type*} [DecidableEq α] {mα : MeasurableSpace α} {ν : Kernel α ℝ}
-  {h : ℕ → α × ℝ} {m n t : ℕ} {a : α}
+variable {α Ω : Type*} [DecidableEq α] {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
+  {ν : Kernel α ℝ}
+  {A : ℕ → Ω → α} {R : ℕ → Ω → ℝ}
+  {ω : Ω} {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]
-
-/-- Gap of an arm `a`: difference between the highest mean of the arms and the mean of `a`. -/
+/-- Gap of an action `a`: difference between the highest mean of the actions and the mean of `a`. -/
 noncomputable
 def gap (ν : Kernel α ℝ) (a : α) : ℝ := (⨆ i, (ν i)[id]) - (ν a)[id]
 
@@ -36,28 +30,35 @@ lemma gap_nonneg [Fintype α] : 0 ≤ gap ν a := by
   rw [gap, sub_nonneg]
   exact le_ciSup (f := fun i ↦ (ν i)[id]) (by simp) a
 
-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
+/-- Regret of a sequence of pulls `k : ℕ → α` at time `t` for the reward kernel `ν ; Kernel α ℝ`. -/
+noncomputable
+def regret (ν : Kernel α ℝ) (A : ℕ → Ω → α) (t : ℕ) (ω : Ω) : ℝ :=
+  t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (A s ω))[id]
+
+omit [DecidableEq α] in
+lemma regret_eq_sum_gap : regret ν A t ω = ∑ s ∈ range t, gap ν (A s ω) := by
+  simp [regret, gap]
 
-lemma arm_eq_of_stepsUntil_eq_coe {ω : ℕ → α × ℝ} (hm : m ≠ 0)
-    (h : stepsUntil a m ω = n) :
-    arm n ω = a := by
-  exact action_eq_of_stepsUntil_eq_coe hm h
+omit [DecidableEq α] in
+lemma regret_nonneg [Fintype α] : 0 ≤ regret ν A t ω := by
+  rw [regret_eq_sum_gap]
+  exact sum_nonneg (fun _ _ ↦ gap_nonneg)
 
-section RewardByCount
+omit [DecidableEq α] in
+lemma gap_eq_zero_of_regret_eq_zero [Fintype α] (hr : regret ν A t ω = 0) {s : ℕ} (hs : s < t) :
+    gap ν (A s ω) = 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 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]
+    regret ν A t ω = ∑ a, pullCount A a t ω * gap ν a := by
+  simp_rw [regret_eq_sum_gap, sum_pullCount_mul]
 
-end RewardByCount
-
-section BestArm
+section bestArm
 
 variable [Fintype α] [Nonempty α]
 
-/-- Arm with the highest mean. -/
+/-- action with the highest mean. -/
 noncomputable def bestArm (ν : Kernel α ℝ) : α :=
   (exists_max_image univ (fun a ↦ (ν a)[id]) (univ_nonempty_iff.mpr inferInstance)).choose
 
@@ -78,6 +79,47 @@ omit [DecidableEq α] in
 lemma gap_bestArm : gap ν (bestArm ν) = 0 := by
   rw [gap_eq_bestArm_sub, sub_self]
 
-end BestArm
+omit [DecidableEq α] in
+lemma integral_eq_of_gap_eq_zero (hg : gap ν a = 0) : (ν (bestArm ν))[id] = (ν a)[id] := by
+  rwa [← sub_eq_zero, ← gap_eq_bestArm_sub]
+
+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 ν A · ω) =o[atTop] fun t ↦ (t : ℝ)) :
+    Tendsto (fun t ↦ (∑ s ∈ range t, (ν (A s ω))[id]) / (t : ℝ))
+      atTop (nhds (⨆ a, (ν a)[id])) := by
+  have ht : Tendsto (fun t ↦ (⨆ a, (ν a)[id]) - regret ν A t ω / 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
+
+/-- If the regret is sublinear, the rate of suboptimal arm pulls tends to zero. -/
+lemma pullCount_rate_tendsto_of_sublinear_regret [Fintype α]
+    (hr : (regret ν A · ω) =o[atTop] fun t ↦ (t : ℝ)) (hg : 0 < gap ν a) :
+    Tendsto (fun t ↦ (pullCount A a t ω : ℝ) / t) atTop (nhds 0) := by
+  have hb (t : ℕ) : (pullCount A a t ω : ℝ) * gap ν a ≤ regret ν A t ω := by
+    rw [regret_eq_sum_pullCount_mul_gap]
+    exact single_le_sum (f := fun a ↦ pullCount A a t ω * gap ν a)
+      (fun _ _ ↦ mul_nonneg (Nat.cast_nonneg _) gap_nonneg) (mem_univ a)
+  have hb' (t : ℕ) : (pullCount A a t ω : ℝ) / t ≤ regret ν A t ω / t / gap ν a := by
+    obtain ht | ht := eq_or_ne t 0
+    · simp [ht]
+    · calc (pullCount A a t ω : ℝ) / t
+          = pullCount A a t ω * gap ν a / gap ν a / t := by field_simp
+        _ ≤ regret ν A t ω / gap ν a / t := by gcongr; exact hb t
+        _ = regret ν A t ω / 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
 
 end Bandits