feat: the eventual regret of ucbF as the Gaussian instance of KL-UCB

LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean

@@ -9,7 +9,6 @@ public import LeanMachineLearning.Online.Bandit.Regret
 public import LMLExplore.Analysis.SpecialFunctions.Log.Basic
 public import LMLExplore.Bandits.Concentration
 public import LMLExplore.Bandits.IndexAlgorithm
-public import LMLExplore.Bandits.Regret
 
 /-!
 # Asymptotically optimal UCB
@@ -48,12 +47,12 @@ Lean round `n` uses `log f(n + 1)`.
   `1 + 5 σ² / ε² + 2 σ² (log f(n) + √(π log f(n)) + 1) / (Δ_a - ε)²` on the expected number of
   pulls of an arm `a` with gap `Δ_a`, for every `ε ∈ (0, Δ_a)`.
 * `ucbF_regret_le`: [LS, Theorem 8.1], the finite-time bound on the expected regret.
-* `UCBF.integral_pullCount_eventually_le`: for an arm `a` with positive gap `Δ_a` and every
-  `c > 2 σ² / Δ_a²`, eventually `E[T_a(n)] ≤ c log n`, that is,
-  `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²`.
-* `ucbF_regret_eventually_le`: [LS, (8.2)], the asymptotic part of [LS, Theorem 8.1]: for every
-  `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, eventually `E[R_n] ≤ c log n`, that is,
-  `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`.
+
+The asymptotic part of [LS, Theorem 8.1], `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`,
+and its form `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²` for the number of pulls, are the Gaussian
+instances of the asymptotic bounds of KL-UCB for exponential families, since `ucbF σ2` is KL-UCB
+for the Gaussian family of variance `σ²`: they are `ucbF_regret_eventually_le` and
+`UCBF.integral_pullCount_eventually_le` in `LMLExplore.Bandits.KLUCB`.
 
 ## Implementation notes
 
@@ -64,10 +63,6 @@ sum, the overestimation of `a` by more than `Δ_a - ε`, is bounded by [LS, Lemm
 i.i.d. reward stream model, by
 `sum_measureReal_action_eq_and_pullCount_eq_zero_or_lt_empMean_add_sqrt_le`.
 
-For the asymptotic bound, `ε` is chosen small enough that `2 σ² / (Δ_a - ε)² < c`. The bound of
-`UCBF.integral_pullCount_le` divided by `log n` then tends to `2 σ² / (Δ_a - ε)²`, since
-`log f(n) / log n → 1` (`Real.tendsto_log_one_add_mul_log_sq_div_log_atTop`).
-
 ## References
 
 * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020,
@@ -265,37 +260,6 @@ theorem ucbF_regret_le
   exact le_ciInf fun ε ↦ mul_le_mul_of_nonneg_left
     (UCBF.integral_pullCount_le h hν hσ2 a ε.2.1 ε.2.2 n) gap_nonneg
 
-/-- **Asymptotic number of pulls of asymptotically optimal UCB.** For σ²-sub-Gaussian rewards
-with `σ² ≠ 0`, an arm `a` with positive gap `Δ_a`, and every `c > 2 σ² / Δ_a²`, the expected
-number of pulls of `a` during the first `n` rounds is eventually at most `c log n`; that is,
-`limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²`. -/
-theorem UCBF.integral_pullCount_eventually_le
-    (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P)
-    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (a : α)
-    (ha : 0 < gap ν a) {c : ℝ} (hc : 2 * σ2 / gap ν a ^ 2 < c) :
-    ∀ᶠ n : ℕ in atTop, P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤ c * log n :=
-  eventually_le_mul_log_of_forall_le_add_mul_add_sqrt_add_one
-    (L := fun n ↦ log (1 + n * log n ^ 2)) ha
-    (tendsto_log_one_add_mul_log_sq_div_log_atTop.comp tendsto_natCast_atTop_atTop) pi_pos.le
-    (fun ε hε ↦ ⟨1 + 5 * σ2 / ε ^ 2, fun n ↦
-      (UCBF.integral_pullCount_le h hν hσ2 a hε.1 hε.2 n).trans_eq (by ring)⟩) hc
-
-/-- **[LS, (8.2)]**, the asymptotic part of [LS, Theorem 8.1]. For σ²-sub-Gaussian rewards with
-`σ² ≠ 0` and every `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, the expected regret of the asymptotically
-optimal UCB algorithm at horizon `n` is eventually at most `c log n`; that is,
-`limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`. -/
-theorem ucbF_regret_eventually_le [StandardBorelSpace α]
-    (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P)
-    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ}
-    (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), 2 * σ2 / gap ν a < c) :
-    ∀ᶠ n : ℕ in atTop, P[regret ν A n] ≤ c * log n := by
-  refine integral_regret_eventually_le_of_forall_integral_pullCount_eventually_le
-    h.measurable_action (.of_forall fun n ↦ log_natCast_nonneg n)
-    (fun a ↦ 2 * σ2 / gap ν a ^ 2)
-    (fun a ha _ hc ↦ UCBF.integral_pullCount_eventually_le h hν hσ2 a ha hc) ?_
-  refine (sum_congr rfl fun a ha ↦ ?_).trans_lt hc
-  field_simp [(mem_filter.mp ha).2.ne']
-
 end Regret
 
 end LMLExplore.Bandits

LMLExplore/Bandits/KLUCB.lean

@@ -82,6 +82,10 @@ Lean round `n` uses `log f(n + 1)`.
   family of every arm with positive gap.
 * `klucbFam_gaussianReal_regret_eventually_le`: for `σ2_a`-sub-Gaussian rewards and the Gaussian
   families of variances `σ2_a`, `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ2_a / Δ_a`.
+* `UCBF.integral_pullCount_eventually_le`, `ucbF_regret_eventually_le`: [LS, (8.2)], the
+  asymptotic part of [LS, Theorem 8.1], as the instance with a common variance `σ²`: for
+  σ²-sub-Gaussian rewards, `ucbF σ2` satisfies `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²` and
+  `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`.
 * `KLUCB.integral_pullCount_le`: for rewards in `[0, 1]`, the bound
   `log f(n) / d(μ_a + ε₁, μ* - ε₂) + 1 / (2 ε₁²) + 2 / ε₂²` on the expected number of pulls of an
   arm `a` with gap `Δ_a`, for all `ε₁, ε₂ > 0` with `ε₁ + ε₂ < Δ_a`.
@@ -141,7 +145,7 @@ this limit to its Exercise 10.2.
 ## References
 
 * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020,
-  Chapter 10.
+  Chapters 8 and 10.
 * [GC11] A. Garivier and O. Cappé, *The KL-UCB algorithm for bounded stochastic bandits and
   beyond*, COLT 2011.
 * [CGMMS13] O. Cappé, A. Garivier, O.-A. Maillard, R. Munos and G. Stoltz, *Kullback–Leibler
@@ -741,6 +745,14 @@ theorem klucbFam_regret_eventually_le [StandardBorelSpace α]
       (by linarith [gap_eq_bestArm_sub (ν := ν) (a := a)]) (hμs a ha) hc)
     (by simpa only [div_eq_mul_inv] using hc)
 
+omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in
+/-- For the Gaussian family of variance `σ2 ≠ 0`, the divergence from the mean of an arm `a` to the
+best mean is `d(μ_a, μ*) = Δ_a² / (2 σ2)`. -/
+lemma expFamilyDiv_gaussianReal_eq_gap_sq (m : ℝ) {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) (a : α) :
+    (gaussianReal m σ2).expFamilyDiv id (ν a)[id] (ν (bestArm ν))[id] =
+      gap ν a ^ 2 / (2 * σ2) := by
+  rw [expFamilyDiv_gaussianReal _ hσ2, ← neg_sub, neg_sq, ← gap_eq_bestArm_sub]
+
 omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in
 /-- For the Gaussian families of variances `σ2 a ≠ 0`, the constant
 `∑_{a : Δ_a > 0} Δ_a / d_{ρ a}(μ_a, μ*)` is `∑_{a : Δ_a > 0} 2 σ2_a / Δ_a`, since
@@ -752,7 +764,7 @@ lemma sum_gap_div_expFamilyDiv_gaussianReal (m : α → ℝ) {σ2 : α → ℝ
   refine sum_congr rfl fun a ha ↦ ?_
   have hga := (mem_filter.mp ha).2
   have hσ2a : (σ2 a : ℝ) ≠ 0 := NNReal.coe_ne_zero.2 (hσ2 a)
-  rw [expFamilyDiv_gaussianReal _ (hσ2 a), ← neg_sub, neg_sq, ← gap_eq_bestArm_sub]
+  rw [expFamilyDiv_gaussianReal_eq_gap_sq _ (hσ2 a)]
   field_simp
 
 /-- **Asymptotic regret of KL-UCB for Gaussian families with known variances.** Let the rewards
@@ -768,17 +780,50 @@ theorem klucbFam_gaussianReal_regret_eventually_le [StandardBorelSpace α] (m :
     {c : ℝ} (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), 2 * σ2 a / gap ν a < c) :
     ∀ᶠ n : ℕ in atTop, P[regret ν A n] ≤ c * log n := by
   -- every arm is dominated on `ℝ` by the member `𝒩(μ_a, σ2 a)` of its family
-  have hdom (a : α) : MGFDominatedOn id (ν a) id ((gaussianReal (m a) (σ2 a)).expFamily id
-      ((gaussianReal (m a) (σ2 a)).natParam id (ν a)[id])) Set.univ := by
-    rw [expFamily_natParam_gaussianReal (m a) (hσ2 a)]
-    exact (hν a).mgfDominatedOn_gaussianReal
+  have hdom (a : α) := (hν a).mgfDominatedOn_expFamily_natParam_gaussianReal (m a) (hσ2 a)
   refine klucbFam_regret_eventually_le h (fun a _ ↦ mem_expFamilyMeans_gaussianReal _ (hσ2 a) _)
     (mem_expFamilyMeans_gaussianReal _ (hσ2 _) _) (fun a _ ↦ (hdom a).mono (Set.subset_univ _))
     ((hdom _).mono (Set.subset_univ _))
     (not_ae_eq_const_gaussianReal _ (hσ2 _))
     (fun a _ ↦ mem_expFamilyMeans_gaussianReal _ (hσ2 a) _) ?_
   exact (sum_gap_div_expFamilyDiv_gaussianReal m hσ2).trans_lt hc
 
+/-- **Asymptotic number of pulls of asymptotically optimal UCB.** For σ²-sub-Gaussian rewards
+with `σ² ≠ 0`, an arm `a` with positive gap `Δ_a`, and every `c > 2 σ² / Δ_a²`, the expected
+number of pulls of `a` by `ucbF σ2` during the first `n` rounds is eventually at most `c log n`;
+that is, `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²`. This is the Gaussian instance of
+`KLUCBFam.integral_pullCount_eventually_le`, since `ucbF σ2` is KL-UCB for the Gaussian family of
+variance `σ²` (`klucbFam_gaussianReal`) and `d(μ_a, μ*) = Δ_a² / (2 σ²)` for that family. -/
+theorem UCBF.integral_pullCount_eventually_le {σ2 : ℝ≥0}
+    (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P)
+    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (a : α)
+    (ha : 0 < gap ν a) {c : ℝ} (hc : 2 * σ2 / gap ν a ^ 2 < c) :
+    ∀ᶠ n : ℕ in atTop, P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤ c * log n := by
+  rw [← klucbFam_gaussianReal 0 hσ2] at h
+  -- every arm is dominated on `ℝ` by the member `𝒩(μ_b, σ2)` of the Gaussian family
+  have hdom (b : α) := (hν b).mgfDominatedOn_expFamily_natParam_gaussianReal 0 hσ2
+  refine KLUCBFam.integral_pullCount_eventually_le (b := bestArm ν) h
+    (mem_expFamilyMeans_gaussianReal _ hσ2 _)
+    ((hdom a).mono (Set.subset_univ _)) (mem_expFamilyMeans_gaussianReal _ hσ2 _)
+    ((hdom _).mono (Set.subset_univ _)) (not_ae_eq_const_gaussianReal _ hσ2)
+    (by linarith [gap_eq_bestArm_sub (ν := ν) (a := a)])
+    (mem_expFamilyMeans_gaussianReal _ hσ2 _) ?_
+  rwa [expFamilyDiv_gaussianReal_eq_gap_sq _ hσ2, inv_div]
+
+/-- **[LS, (8.2)]**, the asymptotic part of [LS, Theorem 8.1]. For σ²-sub-Gaussian rewards with
+`σ² ≠ 0` and every `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, the expected regret of the asymptotically
+optimal UCB algorithm `ucbF σ2` at horizon `n` is eventually at most `c log n`; that is,
+`limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`. This is the instance of
+`klucbFam_gaussianReal_regret_eventually_le` with a common variance, since `ucbF σ2` is KL-UCB for
+the Gaussian family of variance `σ²` (`klucbFam_gaussianReal`). -/
+theorem ucbF_regret_eventually_le [StandardBorelSpace α] {σ2 : ℝ≥0}
+    (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P)
+    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ}
+    (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), 2 * σ2 / gap ν a < c) :
+    ∀ᶠ n : ℕ in atTop, P[regret ν A n] ≤ c * log n := by
+  rw [← klucbFam_gaussianReal 0 hσ2] at h
+  exact klucbFam_gaussianReal_regret_eventually_le (fun _ ↦ 0) h hν (fun _ ↦ hσ2) hc
+
 end FamilyRegret
 
 end LMLExplore.Bandits

LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean

@@ -10,6 +10,7 @@ public import LMLExplore.Probability.Distributions.ExponentialFamily.Invariance
 public import LMLExplore.Probability.Distributions.ExponentialFamily.Posterior.Basic
 public import LMLExplore.Probability.Distributions.ExponentialFamily.UpperConfidence
 public import LMLExplore.Probability.Distributions.Gaussian.Real
+public import LMLExplore.Probability.Moments.MGF.Bound
 public import TauCeti.Probability.Distributions.Tilted
 
 /-!
@@ -74,6 +75,8 @@ Fixed variance, statistic `id`:
 * `LMLExplore.natParam_gaussianReal`: for `v ≠ 0`, the natural parameter of the mean `μ` is
   `(μ - m) / v`.
 * `LMLExplore.expFamily_natParam_gaussianReal`: for `v ≠ 0`, the member of mean `μ` is `𝒩(μ, v)`.
+* `ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal`: if `X - a`
+  is `v`-sub-Gaussian with `v ≠ 0`, then `X` is MGF-dominated on `ℝ` by the member of mean `a`.
 * `LMLExplore.image_expFamily_gaussianReal`: for `v ≠ 0`, the members of the family are the
   Gaussian laws of variance `v`.
 * `LMLExplore.expFamilyDiv_gaussianReal`: for `v ≠ 0`, the divergence of the family is
@@ -208,6 +211,16 @@ theorem expFamily_natParam_gaussianReal (m : ℝ) (hv : v ≠ 0) (μ : ℝ) :
   field_simp
   ring
 
+/-- If `X - a` is `σ2`-sub-Gaussian with `σ2 ≠ 0`, then `X` is dominated on `ℝ` by the member of
+mean `a` of the Gaussian family of variance `σ2` generated by any `𝒩(m, σ2)`. -/
+lemma _root_.ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal
+    {β : Type*} {mβ : MeasurableSpace β} {X : β → ℝ} {Q : Measure β} {a : ℝ} {σ2 : ℝ≥0}
+    (h : HasSubgaussianMGF (fun x ↦ X x - a) σ2 Q) (m : ℝ) (hσ2 : σ2 ≠ 0) :
+    MGFDominatedOn X Q id ((gaussianReal m σ2).expFamily id ((gaussianReal m σ2).natParam id a))
+      Set.univ := by
+  rw [expFamily_natParam_gaussianReal m hσ2]
+  exact h.mgfDominatedOn_gaussianReal
+
 /-- For `v ≠ 0`, the members of the exponential family of `𝒩(m, v)` are the Gaussian laws
 `𝒩(μ, v)` of variance `v`, for every mean `μ`. -/
 theorem image_expFamily_gaussianReal (m : ℝ) (hv : v ≠ 0) :