Bandits: state regret with LML's gap, move general lemmas to ForMathlib/ForLML

pseudoRegret takes the reward kernel, as LML's regret does, and the ETC,
UCB and ε-greedy bounds are stated with LML's gap, replacing gapOf.

General lemmas move out of Bandits.Theory into files mirroring their
upstream homes, generalized where the statement allows: RandomDo/ForMathlib
(map_compProd_eq_bind, bind_map, Measurable.finSnoc,
hasSubgaussianMGF_gaussianReal) and RandomDo/ForLML (pullCount'_snoc,
sumRewards'_snoc, IT.hist_succ_eq_snoc, IT.map_hist_succ). The Vector
measurability lemmas join RandomDo.Measurable. Duplicates are removed:
RDo.map_compProd and RDo.bind_map of Trace.lean are now the ForMathlib
lemmas, and LML's Measure.dirac_compProd replaces dirac_compProd_eq_map.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: RemyDegenne

Bandits/EpsGreedy.lean

@@ -209,13 +209,13 @@ lemma policy_eq_epsGreedyArm (n : ℕ) (h : Hist Unit (Fin K) ℝ n) :
 /-- **ε-greedy has linear regret**, for the program that runs: the expected pseudo-regret of
 `banditRunRand` with `epsGreedyArm`, against Gaussian arms, is at least `n ε / K ∑ₐ Δₐ`. -/
 theorem le_integral_regret_banditRunRand (μ : Fin K → ℝ) (σ2 : ℝ≥0) (n : ℕ) :
-    (n : ℝ) * ((ε : ℝ) / K) * ∑ a, gapOf μ a
-      ≤ ∫ s, pseudoRegret μ s
+    (n : ℝ) * ((ε : ℝ) / K) * ∑ a, gap (arms μ σ2) a
+      ≤ ∫ s, pseudoRegret (arms μ σ2) s
           ∂(banditRunRand (m := Measure) (epsGreedyArm (m := Measure) (ε : ℝ)) μ σ2 n) := by
   rw [integral_pseudoRegret_banditRunRand μ σ2 (alg ε) _ (isMarkov_epsGreedyArm ε)
     (policy_eq_epsGreedyArm ε) n]
   have h := le_integral_regret ε (arms μ σ2)
     (IT.isAlgEnvSeq_trajMeasure (alg (K := K) ε) (stationaryEnv (arms μ σ2))) n
-  simpa only [gap_arms] using h
+  exact h
 
 end RDoBandit.EpsGreedy

Bandits/Theory.lean

@@ -1,6 +1,13 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import RandomDo.ForLML.SequentialLearning.FiniteActions
+public import RandomDo.ForLML.SequentialLearning.IonescuTulceaSpace
+public import RandomDo.ForLML.SequentialLearning.SumRewards
+public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Constructions
 public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
+public import RandomDo.ForMathlib.MeasureTheory.Measure.GiryMonad
+public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp
+public import RandomDo.ForMathlib.Probability.Moments.SubGaussian
 public import RandomDo.Measurable
 public import RandomDo.Monad.ForInInstances
 public import RandomDo.Monad.Instances

RandomDo.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.FiniteActions
+
+/-!
+# The number of pulls of an action, one round later
+
+## Main results
+
+* `pullCount'_snoc`: the number of pulls of an action in a history extended by one round.
+-/
+
+@[expose] public section
+
+namespace Learning
+
+variable {𝓞 𝓐 𝓨 : Type*} [DecidableEq 𝓐]
+
+lemma pullCount'_snoc (n : ℕ) (h : Hist 𝓞 𝓐 𝓨 n) (o : 𝓞) (a b : 𝓐) (y : 𝓨) :
+    pullCount' (n + 1) (Fin.snoc h (o, a, y)) b = pullCount' n h b + if a = b then 1 else 0 := by
+  rw [pullCount'_eq_sum, pullCount'_eq_sum, Fin.sum_univ_castSucc]
+  simp [Fin.snoc_castSucc, Fin.snoc_last]
+
+end Learning

RandomDo/ForLML/SequentialLearning/FiniteActions.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Constructions
+public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp
+
+/-!
+# The history of the interaction, one round later
+
+## Main results
+
+* `IT.hist_succ_eq_snoc`: the history before time `n + 1` is the history before time `n`, followed
+  by the round at time `n`.
+* `IT.map_hist_succ`: under `trajMeasure alg env`, the law of a function of the history before
+  time `n + 1` is the law of the history before time `n`, bound to one round drawn from the step
+  kernel.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory
+
+namespace Learning.IT
+
+variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐}
+  {m𝓨 : MeasurableSpace 𝓨}
+
+lemma hist_succ_eq_snoc (n : ℕ) :
+    hist (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) (n + 1) = fun ω ↦ Fin.snoc (hist n ω) (step n ω) := by
+  funext ω i
+  refine Fin.lastCases ?_ (fun j ↦ ?_) i
+  · simp [hist, step]
+  · simp [hist]
+
+/-- The history before time `n + 1` is the history before time `n`, followed by one round drawn
+from the step kernel. -/
+lemma map_hist_succ {γ : Type*} [MeasurableSpace γ] (alg : Algorithm 𝓞 𝓐 𝓨)
+    (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) {F : Hist 𝓞 𝓐 𝓨 (n + 1) → γ} (hF : Measurable F) :
+    (trajMeasure alg env).map (F ∘ hist (n + 1))
+      = ((trajMeasure alg env).map (hist n)).bind
+          fun h ↦ (stepKernel alg env n h).map fun x ↦ F (Fin.snoc h x) := by
+  have hsnoc : Measurable fun p : Hist 𝓞 𝓐 𝓨 n × Round 𝓞 𝓐 𝓨 ↦ F (Fin.snoc p.1 p.2) :=
+    hF.comp (measurable_fst.finSnoc measurable_snd)
+  have e : F ∘ hist (n + 1)
+      = (fun p ↦ F (Fin.snoc p.1 p.2)) ∘ (fun ω ↦ (hist n ω, step n ω)) := by
+    rw [hist_succ_eq_snoc]
+    rfl
+  rw [e, ← Measure.map_map hsnoc (by fun_prop), (hasCondDistrib_step alg env n).map_eq,
+    Measure.map_compProd_eq_bind _ _ hsnoc]
+
+end Learning.IT

RandomDo/ForLML/SequentialLearning/IonescuTulceaSpace.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.SumRewards
+
+/-!
+# The sum of the rewards of an action, one round later
+
+## Main results
+
+* `sumRewards'_snoc`: the sum of the rewards of an action in a history extended by one round.
+-/
+
+@[expose] public section
+
+namespace Learning
+
+variable {𝓞 𝓐 𝓨 : Type*} [DecidableEq 𝓐] [AddCommGroup 𝓨]
+
+lemma sumRewards'_snoc (n : ℕ) (h : Hist 𝓞 𝓐 𝓨 n) (o : 𝓞) (a b : 𝓐) (y : 𝓨) :
+    sumRewards' (n + 1) (Fin.snoc h (o, a, y)) b = sumRewards' n h b + if a = b then y else 0 := by
+  rw [sumRewards', sumRewards', Fin.sum_univ_castSucc]
+  simp [Fin.snoc_castSucc, Fin.snoc_last]
+
+end Learning

RandomDo/ForLML/SequentialLearning/SumRewards.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.MeasurableSpace.Constructions
+
+/-!
+# Measurability of `Fin.snoc`
+
+## Main results
+
+* `Measurable.finSnoc`: appending an element to a tuple is measurable, the measurable counterpart
+  of `Continuous.finSnoc`.
+-/
+
+@[expose] public section
+
+variable {α : Type*} [MeasurableSpace α] {n : ℕ} {X : Fin (n + 1) → Type*}
+  [∀ i, MeasurableSpace (X i)]
+
+@[fun_prop]
+lemma Measurable.finSnoc {f : α → ∀ j : Fin n, X j.castSucc} {g : α → X (Fin.last n)}
+    (hf : Measurable f) (hg : Measurable g) : Measurable fun a ↦ Fin.snoc (f a) (g a) := by
+  refine measurable_pi_iff.2 fun i ↦ ?_
+  refine Fin.lastCases ?_ (fun j ↦ ?_) i
+  · simpa only [Fin.snoc_last] using hg
+  · simp only [Fin.snoc_castSucc]
+    exact (measurable_pi_apply j).comp hf

RandomDo/ForMathlib/MeasureTheory/MeasurableSpace/Constructions.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.GiryMonad
+
+/-!
+# Binding a pushforward measure
+
+## Main results
+
+* `Measure.bind_map`: binding after mapping is binding the composite, the measure counterpart of
+  `PMF.bind_map`.
+-/
+
+@[expose] public section
+
+namespace MeasureTheory.Measure
+
+variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+
+/-- `Measure.bind` sees through a `Measure.map` on the left. -/
+lemma bind_map (μ : Measure α) {f : α → β} (hf : Measurable f) {k : β → Measure γ}
+    (hk : Measurable k) : (μ.map f).bind k = μ.bind fun a ↦ k (f a) := by
+  rw [Measure.bind, Measure.bind, map_map hk hf]
+  rfl
+
+end MeasureTheory.Measure

RandomDo/ForMathlib/MeasureTheory/Measure/GiryMonad.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Kernel.Composition.MeasureComp
+
+/-!
+# Pushforwards of the composition-product of a measure and a kernel
+
+## Main results
+
+* `Measure.map_compProd_eq_bind`: mapping `μ ⊗ₘ κ` along `g` is binding `κ a` mapped along the
+  section `g (a, ·)`.
+-/
+
+@[expose] public section
+
+open ProbabilityTheory
+
+namespace MeasureTheory.Measure
+
+variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+
+/-- Mapping a composition-product is binding the kernel, mapped along the section. -/
+lemma map_compProd_eq_bind (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsSFiniteKernel κ]
+    {g : α × β → γ} (hg : Measurable g) :
+    (μ ⊗ₘ κ).map g = μ.bind fun a ↦ (κ a).map fun b ↦ g (a, b) := by
+  rw [compProd_eq_comp_prod, map_comp _ _ hg]
+  refine bind_congr_right (.of_forall fun a ↦ ?_)
+  rw [Kernel.map_apply _ hg, Kernel.prod_apply, Kernel.id_apply, dirac_prod,
+    map_map hg measurable_prodMk_left]
+  rfl
+
+end MeasureTheory.Measure

RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Distributions.Gaussian.Real
+public import Mathlib.Probability.Moments.SubGaussian
+
+/-!
+# Gaussian distributions are sub-Gaussian
+
+## Main results
+
+* `hasSubgaussianMGF_gaussianReal`: centered, a Gaussian is sub-Gaussian with variance proxy its
+  variance.
+-/
+
+@[expose] public section
+
+open MeasureTheory
+open scoped NNReal
+
+namespace ProbabilityTheory
+
+/-- Centered, a Gaussian is sub-Gaussian with variance proxy its variance. -/
+lemma hasSubgaussianMGF_gaussianReal (μ : ℝ) (v : ℝ≥0) :
+    HasSubgaussianMGF (fun x ↦ x - μ) v (gaussianReal μ v) := by
+  refine ⟨fun t ↦ ?_, fun t ↦ ?_⟩
+  · have := (integrable_exp_mul_gaussianReal (μ := μ) (v := v) t).const_mul (Real.exp (-(t * μ)))
+    refine this.congr (Filter.Eventually.of_forall fun x ↦ ?_)
+    simp only
+    rw [← Real.exp_add]
+    ring_nf
+  · rw [mgf_gaussianReal ⟨by fun_prop, gaussianReal_map_sub_const μ⟩ t]
+    simp
+
+end ProbabilityTheory