feat: large deviations of the empirical means of a run under static allocations, and the error exponent of static proportions

LMLExplore/Analysis/SpecificLimits/Basic.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.Analysis.Normed.Group.Continuity
+public import Mathlib.Analysis.Normed.Group.Real
+public import Mathlib.Analysis.SpecificLimits.Basic
+
+/-!
+# Limits of ratios to `n` of sequences within bounded distance of a linear sequence
+
+A real sequence `u` that stays within a fixed distance `c` of the linear sequence `n ↦ n w`
+satisfies `u n / n → w`. Numbers of pulls of bandit algorithms that track static proportions `w`
+up to a bounded error have this form.
+
+## Main statements
+
+* `LMLExplore.tendsto_div_natCast_of_abs_sub_mul_le`: if `|u n - n w| ≤ c` for every `n`, then
+  `u n / n → w`.
+-/
+
+public section
+
+open Filter Topology
+
+namespace LMLExplore
+
+/-- If `|u n - n w| ≤ c` for every `n`, then `u n / n → w`. -/
+theorem tendsto_div_natCast_of_abs_sub_mul_le {u : ℕ → ℝ} {w c : ℝ}
+    (h : ∀ n : ℕ, |u n - n * w| ≤ c) : Tendsto (fun n : ℕ ↦ u n / n) atTop (𝓝 w) := by
+  have h0 : Tendsto (fun n : ℕ ↦ (u n - n * w) / n) atTop (𝓝 0) := by
+    refine squeeze_zero_norm (fun n ↦ ?_) (tendsto_const_div_atTop_nhds_zero_nat c)
+    rw [Real.norm_eq_abs, abs_div, Nat.abs_cast]
+    exact div_le_div_of_nonneg_right (h n) n.cast_nonneg
+  have h1 : Tendsto (fun n : ℕ ↦ (u n - n * w) / n + w) atTop (𝓝 w) := by
+    simpa using h0.add_const w
+  refine h1.congr' ?_
+  filter_upwards [eventually_ne_atTop 0] with n hn
+  rw [sub_div, mul_div_cancel_left₀ _ (Nat.cast_ne_zero.2 hn), sub_add_cancel]
+
+end LMLExplore

LMLExplore/Identification/StaticProportions.lean

@@ -7,6 +7,7 @@ module
 
 public import LMLExplore.Identification.CumulativeTracking
 public import LMLExplore.Identification.DifficultyRatio
+public import LMLExplore.SequentialLearning.StaticAllocation
 public import LeanMachineLearning.SequentialLearning.SumRewards
 
 /-!
@@ -56,6 +57,19 @@ in exponential families and a regular task [D23, Theorem 1].
 * `LMLExplore.Identification.IdentTask.IsStaticProportions.errorProb_eq`: the probability of error
   of a static proportions family is the probability that the recommendation of the empirical means
   is not correct.
+* `LMLExplore.Identification.IdentTask.IsStaticProportions.hasLDP_empMean`: for arms whose
+  cumulant generating functions are finite near `0`, the laws of the empirical means of a static
+  proportions family satisfy the large deviation principle with rate function
+  `x ↦ ∑ a, w a I_a(x a)`, for the Cramér rate functions `I_a` of the arms.
+* `LMLExplore.Identification.IdentTask.IsStaticProportions.limsup_log_errorProb_div_le`,
+  `LMLExplore.Identification.IdentTask.IsStaticProportions.neg_le_liminf_log_errorProb_div`: the
+  error exponent of a static proportions family is between the infima of `∑ a, w a I_a(x a)` over
+  the interior and over the closure of the set of the vectors `x` whose recommendation `rec x` is
+  not correct [GJ04; D23, Theorem 12].
+* `LMLExplore.Identification.IdentTask.IsStaticProportions.tendsto_log_errorProb_div`,
+  `LMLExplore.Identification.IdentTask.IsStaticProportions.tendsto_errorComplexity`: when the two
+  infima agree, the error exponent is their common value `c`, and the error complexity
+  `T / log (1 / p_{θ,T})` tends to `c⁻¹`.
 
 ## References
 
@@ -71,9 +85,10 @@ in exponential families and a regular task [D23, Theorem 1].
 
 public section
 
-open MeasureTheory Learning
+open MeasureTheory Learning Filter Topology ProbabilityTheory
+open TauCeti.Probability (HasLDP)
 
-open scoped ENNReal
+open scoped ENNReal NNReal
 
 namespace LMLExplore.Identification.IdentTask
 
@@ -250,4 +265,105 @@ lemma IsStaticProportions.errorProb_eq (h𝒜 : task.IsStaticProportions rec 
     lintegral_map (ProbabilityTheory.Kernel.measurable_coe _ hθ.compl) (IT.measurable_hist T),
     lintegral_congr heq, lintegral_indicator_one hE]
 
+/-! ### The error exponent of static proportions families -/
+
+variable [MeasurableSingletonClass α] {θ : Θ}
+
+/-- **Large deviations of the empirical means of a static proportions family** [GJ04;
+D23, Theorem 12]. If the cumulant generating function of each arm of the admissible model `θ` is
+finite on a neighbourhood of `0`, the laws of the vectors of the empirical means after `T` rounds
+of a static proportions family with proportions `w` satisfy the large deviation principle with
+speed `1 / T` and rate function `x ↦ ∑ a, w a I_a(x a)`, with `I_a` the Cramér rate function of
+the law `ν_a(θ)` of arm `a`. -/
+theorem IsStaticProportions.hasLDP_empMean (h𝒜 : task.IsStaticProportions rec 𝒜 w)
+    (hθ : θ ∈ task.M) (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) :
+    HasLDP atTop (fun T : ℕ ↦ (T : ℝ≥0)⁻¹)
+      (fun T ↦ (trajMeasure (𝒜 T).alg (Environment.bandit (task.ν θ))).map
+        fun h a ↦ empMean IT.action IT.feedback a T h)
+      (fun x ↦ ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a)) :=
+  hasLDP_empMean_rateFunction_of_abs_pullCount_sub_le hν h𝒜.pos (Fintype.card α)
+    (fun T ↦ IT.isAlgEnvSeq_trajMeasure (𝒜 T).alg (Environment.bandit (task.ν θ)))
+    (h𝒜.ae_abs_pullCount_sub_le θ hθ)
+
+/-- **Upper bound on the error exponent of a static proportions family** [GJ04; D23, Theorem 12].
+If the set of correct answers of the admissible model `θ` is measurable and the cumulant generating
+function of each of its arms is finite on a neighbourhood of `0`, the probability of error
+`p_{θ,T}` of a static proportions family with proportions `w` and recommendation rule `rec`
+satisfies `limsup_T (1 / T) log p_{θ,T} ≤ -inf_x ∑ a, w a I_a(x a)`, the infimum over the closure
+of the set of the vectors `x` with `rec x` not correct for `θ`, with `I_a` the Cramér rate function
+of the law `ν_a(θ)` of arm `a`. -/
+theorem IsStaticProportions.limsup_log_errorProb_div_le (h𝒜 : task.IsStaticProportions rec 𝒜 w)
+    (hθ : θ ∈ task.M) (hcorrect : MeasurableSet (task.correct θ))
+    (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) :
+    limsup (fun T : ℕ ↦ ENNReal.log (task.errorProb 𝒜 θ T) / T) atTop ≤
+      -((⨅ x ∈ closure {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) : ℝ≥0∞) : EReal) := by
+  have h := (h𝒜.hasLDP_empMean hθ hν).limsup_le_neg_iInf_closure {x | rec x ∉ task.correct θ}
+  simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h
+  refine le_trans (limsup_le_limsup (Eventually.of_forall fun T ↦ ?_)) h
+  -- The error is the event that the empirical means lie in the set where `rec` is not correct.
+  rw [h𝒜.errorProb_eq hcorrect]
+  exact EReal.div_le_div_right_of_nonneg (by positivity) (ENNReal.log_monotone
+    (Measure.le_map_apply
+      (measurable_empMean_pi IT.measurable_action IT.measurable_feedback T).aemeasurable
+      {x | rec x ∉ task.correct θ}))
+
+/-- **Lower bound on the error exponent of a static proportions family** [GJ04; D23, Theorem 12].
+If the set of correct answers of the admissible model `θ` is measurable and the cumulant generating
+function of each of its arms is finite on a neighbourhood of `0`, the probability of error
+`p_{θ,T}` of a static proportions family with proportions `w` and recommendation rule `rec`
+satisfies `-inf_x ∑ a, w a I_a(x a) ≤ liminf_T (1 / T) log p_{θ,T}`, the infimum over the
+interior of the set of the vectors `x` with `rec x` not correct for `θ`, with `I_a` the Cramér rate
+function of the law `ν_a(θ)` of arm `a`. -/
+theorem IsStaticProportions.neg_le_liminf_log_errorProb_div
+    (h𝒜 : task.IsStaticProportions rec 𝒜 w) (hθ : θ ∈ task.M)
+    (hcorrect : MeasurableSet (task.correct θ))
+    (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a))) :
+    -((⨅ x ∈ interior {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) : ℝ≥0∞) : EReal) ≤
+      liminf (fun T : ℕ ↦ ENNReal.log (task.errorProb 𝒜 θ T) / T) atTop := by
+  have h := (h𝒜.hasLDP_empMean hθ hν).lower_bound (interior {x | rec x ∉ task.correct θ})
+    isOpen_interior
+  simp_rw [EReal.coe_nnreal_inv_natCast_mul] at h
+  refine h.trans (liminf_le_liminf (Eventually.of_forall fun T ↦ ?_))
+  -- The empirical means in the interior of the set where `rec` is not correct give an error.
+  rw [h𝒜.errorProb_eq hcorrect, Measure.map_apply
+    (measurable_empMean_pi IT.measurable_action IT.measurable_feedback T)
+    isOpen_interior.measurableSet]
+  exact EReal.div_le_div_right_of_nonneg (by positivity)
+    (ENNReal.log_monotone (measure_mono (Set.preimage_mono interior_subset)))
+
+/-- **The error exponent of a static proportions family** [GJ04; D23, Theorem 12]. If moreover the
+infima of `x ↦ ∑ a, w a I_a(x a)` over the interior and over the closure of the set of the vectors
+`x` with `rec x` not correct for `θ` agree, then `(1 / T) log p_{θ,T}` tends to minus their common
+value. -/
+theorem IsStaticProportions.tendsto_log_errorProb_div (h𝒜 : task.IsStaticProportions rec 𝒜 w)
+    (hθ : θ ∈ task.M) (hcorrect : MeasurableSet (task.correct θ))
+    (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a)))
+    (h_eq : ⨅ x ∈ interior {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) =
+      ⨅ x ∈ closure {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a)) :
+    Tendsto (fun T : ℕ ↦ ENNReal.log (task.errorProb 𝒜 θ T) / T) atTop
+      (𝓝 (-((⨅ x ∈ closure {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) : ℝ≥0∞) : EReal))) :=
+  tendsto_of_le_liminf_of_limsup_le (h_eq ▸ h𝒜.neg_le_liminf_log_errorProb_div hθ hcorrect hν)
+    (h𝒜.limsup_log_errorProb_div_le hθ hcorrect hν)
+
+/-- **The error complexity of a static proportions family** [D23, Theorem 12]. Under the hypotheses
+of `IsStaticProportions.tendsto_log_errorProb_div`, the error complexity `T / log (1 / p_{θ,T})`
+tends to the inverse of the error exponent `inf_x ∑ a, w a I_a(x a)`. -/
+theorem IsStaticProportions.tendsto_errorComplexity (h𝒜 : task.IsStaticProportions rec 𝒜 w)
+    (hθ : θ ∈ task.M) (hcorrect : MeasurableSet (task.correct θ))
+    (hν : ∀ a, 0 ∈ interior (integrableExpSet id (task.ν θ a)))
+    (h_eq : ⨅ x ∈ interior {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a) =
+      ⨅ x ∈ closure {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a)) :
+    Tendsto (task.errorComplexity 𝒜 θ) atTop
+      (𝓝 (⨅ x ∈ closure {x | rec x ∉ task.correct θ},
+        ∑ a, ENNReal.ofReal (w a) * rateFunction id (task.ν θ a) (x a))⁻¹) :=
+  tendsto_errorComplexity_of_tendsto_log_div
+    (h𝒜.tendsto_log_errorProb_div hθ hcorrect hν h_eq)
+
 end LMLExplore.Identification.IdentTask

LMLExplore/Probability/LargeDeviations/Pi.lean

@@ -40,6 +40,8 @@ rates is above `r`.
 
 * `LMLExplore.hasLDP_pi`: the large deviation principle of the product measures, with
   rate function `x ↦ ∑ a, I a (x a)`.
+* `LMLExplore.neg_sum_le_liminf_log_pi`: the lower bound of the product principle at a point,
+  for laws satisfying large deviation principles whose rate functions need not be good.
 * `LMLExplore.hasLDP_pi_comp_of_tendsto_div`: the large deviation principle of the
   product measures `Measure.pi fun a ↦ P a (m a n)` with `m a n / n → w a > 0`, with rate function
   `x ↦ ∑ a, w a I a (x a)`.
@@ -86,10 +88,11 @@ private lemma ofReal_exp_neg_mul_le (n : ℕ) {r r' : ℝ} (h : r ≤ r') :
 variable {ι : Type*} [Fintype ι] {X : ι → Type*} [∀ a, MeasurableSpace (X a)]
   {P : ∀ a, ℕ → Measure (X a)} {I : ∀ a, X a → ℝ≥0∞}
 
-/-- **The lower bound of the product principle.** If each `P a` satisfies the lower bound of a
-large deviation principle at the speed `1 / n` with rate function `I a`, every neighbourhood `s`
-of a point `x` satisfies `-∑ a, I a (x a) ≤ liminf_n (1 / n) log (∏ a, P a n) s`. -/
-private lemma neg_sum_le_liminf_log_pi [∀ a, TopologicalSpace (X a)]
+/-- **The lower bound of the product principle.** If each `P a` satisfies a large deviation
+principle at the speed `1 / n` with rate function `I a` (goodness of `I a` is not needed),
+every neighbourhood `s` of a point `x` satisfies
+`-∑ a, I a (x a) ≤ liminf_n (1 / n) log (∏ a, P a n) s`. -/
+theorem neg_sum_le_liminf_log_pi [∀ a, TopologicalSpace (X a)]
     [∀ a n, SigmaFinite (P a n)] (h : ∀ a, HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) (P a) (I a))
     {x : ∀ a, X a} {s : Set (∀ a, X a)} (hs : s ∈ 𝓝 x) :
     -((∑ a, I a (x a) : ℝ≥0∞) : EReal) ≤ liminf (fun n : ℕ ↦

LMLExplore/Probability/ProductMeasure.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.Probability.Independence.InfinitePi
+
+/-!
+# Infinite products of probability measures: the first terms and the next terms
+
+Under the infinite product `Measure.infinitePi` of copies of a probability measure `μ`, the first
+`n` coordinates and the next `m` coordinates are independent.
+
+## Main statements
+
+* `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the
+  first `n` terms and the next `m` terms are independent.
+-/
+
+public section
+
+namespace MeasureTheory.Measure
+
+open ProbabilityTheory Finset in
+/-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d.
+sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie
+in `C` with probability `μ^⊗n(B) μ(C)^m`. -/
+theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X)
+    [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B)
+    (hC : MeasurableSet C) :
+    (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} =
+      Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by
+  -- The first `n` terms and the next `m` terms are independent.
+  have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id)
+    (fun _ ↦ measurable_id)).indepFun_finset (range n) (Ico n (n + m))
+    (Finset.disjoint_left.2 fun i hi hi' ↦ by simp at hi hi'; omega) (fun _ ↦ by fun_prop)
+  simp only [id] at h_ind
+  have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦
+      u ⟨i, mem_range.2 i.2⟩ := by fun_prop
+  have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} =
+      (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩
+        (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by
+    ext z
+    simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi,
+      Set.mem_univ, true_implies, Subtype.forall, mem_Ico]
+    refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩
+    obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1
+    exact h j (by omega)
+  rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)]
+  congr 1
+  · -- The first `n` terms are `n` independent samples of `μ`.
+    have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) =
+        Measure.pi fun _ : Fin n ↦ μ := by
+      rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi]
+    rw [← h_pi, Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp]
+    -- Both sides are the preimage of `B` under `z ↦ (z i)_{i : Fin n}`: the composite
+    -- `(fun u i ↦ u ⟨i, _⟩) ∘ (fun z i ↦ z i)` unfolds to `fun z i ↦ z ↑⟨i, _⟩`, and
+    -- `↑⟨i, _⟩ = i` is `Subtype.val` applied to a constructor.
+    rfl
+  · have h_pi : (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) =
+        ((Ico n (n + m) : Finset ℕ) : Set ℕ).pi fun _ ↦ C := by
+      ext z
+      simp
+    rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico,
+      Nat.add_sub_cancel_left]
+
+end MeasureTheory.Measure