Basic regret properties

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 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]
+
+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, sum_pullCount_mul, arm, action]
 
 end RewardByCount
 
@@ -73,11 +88,51 @@ 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_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]
 lemma gap_bestArm : gap ν (bestArm ν) = 0 := by
   rw [gap_eq_bestArm_sub, sub_self]
 
 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
+  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
+
+/-- 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
+  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; exact hb t
+        _ = 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
+
 end Bandits