diff --git a/LeanBandits.lean b/LeanBandits.lean
index c1a8f31c..542cff67 100644
--- a/LeanBandits.lean
+++ b/LeanBandits.lean
@@ -10,6 +10,7 @@ import LeanBandits.ForMathlib.CondIndepFun
 import LeanBandits.ForMathlib.HasCondDistrib
 import LeanBandits.ForMathlib.IndepFun
 import LeanBandits.ForMathlib.IndepInfinitePi
+import LeanBandits.ForMathlib.Integrable
 import LeanBandits.ForMathlib.KernelRepresentation
 import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Measurable
diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean
index 27f62a02..67b8f986 100644
--- a/LeanBandits/Bandit/Bandit.lean
+++ b/LeanBandits/Bandit/Bandit.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne, Paulo Rauber
 import LeanBandits.ForMathlib.CondIndepFun
 import LeanBandits.ForMathlib.IndepFun
 import LeanBandits.ForMathlib.IndepInfinitePi
+import LeanBandits.ForMathlib.Integrable
 import LeanBandits.ForMathlib.KernelRepresentation
 import LeanBandits.ForMathlib.StandardBorel
 import LeanBandits.SequentialLearning.FiniteActions
@@ -59,16 +60,6 @@ lemma identDistrib_eval_eval_id_streamMeasure (ν : Kernel α R) [IsMarkovKernel
       Measure.map_map (by fun_prop) (by fun_prop)]
     simp
 
-lemma Integrable.congr_identDistrib {Ω Ω' : Type*}
-    {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
-    {μ : Measure Ω} {μ' : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ}
-    (hX : Integrable X μ) (hXY : IdentDistrib X Y μ μ') :
-    Integrable Y μ' := by
-  have hX' : Integrable id (μ.map X) := by
-    rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_fst]
-  rw [hXY.map_eq] at hX'
-  rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_snd] at hX'
-
 lemma integrable_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n : ℕ) (a : α)
     (h_int : Integrable id (ν a)) :
     Integrable (fun h : ℕ → α → ℝ ↦ h n a) (streamMeasure ν) :=
diff --git a/LeanBandits/Bandit/Regret.lean b/LeanBandits/Bandit/Regret.lean
index fdbfb8da..28f1ec97 100644
--- a/LeanBandits/Bandit/Regret.lean
+++ b/LeanBandits/Bandit/Regret.lean
@@ -54,6 +54,33 @@ lemma regret_eq_sum_pullCount_mul_gap [Fintype α] :
     regret ν A t ω = ∑ a, pullCount A a t ω * gap ν a := by
   simp_rw [regret_eq_sum_gap, sum_pullCount_mul]
 
+lemma integral_regret_eq_sum_gap_mul_integral_pullCount
+    [StandardBorelSpace α] [Fintype α] {P : Measure Ω} [IsProbabilityMeasure P]
+    (hA : ∀ n, Measurable (A n)) :
+    P[regret ν A n] = ∑ a, gap ν a * P[fun ω ↦ (pullCount A a n ω : ℝ)] := by
+  simp_rw [regret_eq_sum_pullCount_mul_gap]
+  rw [integral_finset_sum]
+  swap; · exact fun i _ ↦ (integrable_pullCount hA i n).mul_const _
+  congr with a
+  rw [integral_mul_const, mul_comm]
+
+/-- To bound the expected regret, it suffices to bound the expected number of pulls for each action
+with positive gap. -/
+lemma integral_regret_le_of_forall_integral_pullCount_le
+    [Nonempty α] [StandardBorelSpace α] [Fintype α] {P : Measure Ω} [IsProbabilityMeasure P]
+    {alg : Algorithm α ℝ} {env : Environment α ℝ} {B : α → ℝ}
+    (h : IsAlgEnvSeq A R alg env P)
+    (h_le : ∀ a, gap ν a ≠ 0 → ∫ ω, (pullCount A a n ω : ℝ) ∂P ≤ B a) :
+    P[regret ν A n] ≤ ∑ a, gap ν a * B a := by
+  have hA := h.measurable_A
+  rw [integral_regret_eq_sum_gap_mul_integral_pullCount hA]
+  gcongr 1 with a
+  by_cases h_gap : gap ν a = 0
+  · simp [h_gap]
+  gcongr
+  · exact gap_nonneg
+  · exact h_le a h_gap
+
 section bestArm
 
 variable [Fintype α] [Nonempty α]
diff --git a/LeanBandits/Bandit/RewardByCountMeasure.lean b/LeanBandits/Bandit/RewardByCountMeasure.lean
index bb0b4b35..b8dae4dd 100644
--- a/LeanBandits/Bandit/RewardByCountMeasure.lean
+++ b/LeanBandits/Bandit/RewardByCountMeasure.lean
@@ -20,14 +20,14 @@ variable {α Ω : Type*} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [
   {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν]
   {h_inter : IsAlgEnvSeq A R alg (stationaryEnv ν) P}
 
-local notation "𝔓'" => P.prod (streamMeasure ν)
+local notation "𝔓" => P.prod (streamMeasure ν)
 
 omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in
 lemma hasLaw_Z (a : α) (m : ℕ) :
-  HasLaw (fun ω ↦ ω.2 m a) (ν a) 𝔓' where
+  HasLaw (fun ω ↦ ω.2 m a) (ν a) 𝔓 where
   map_eq := by
-    calc (𝔓').map (fun ω ↦ ω.2 m a)
-    _ = ((𝔓').snd).map (fun ω ↦ ω m a) := by
+    calc (𝔓).map (fun ω ↦ ω.2 m a)
+    _ = ((𝔓).snd).map (fun ω ↦ ω m a) := by
       rw [Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)]
       rfl
     _ = (streamMeasure ν).map (fun ω ↦ ω m a) := by simp
@@ -47,15 +47,15 @@ notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹'
 omit [DecidableEq α] in
 lemma condDistrib_reward'' [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (n : ℕ) :
-    𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓'] =ᵐ[(𝔓').map (fun ω ↦ A n ω.1)] ν := by
+    𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓] =ᵐ[(𝔓).map (fun ω ↦ A n ω.1)] ν := by
   have hA := h.measurable_A
   have hR := h.measurable_R
   have h_ra' : 𝓛[R n | A n; P] =ᵐ[P.map (A n)] ν := h.condDistrib_reward_stationaryEnv n
-  have h_law : (𝔓').map (fun ω ↦ A n ω.1) = P.map (A n) := by
-    change ((𝔓').map (A n ∘ Prod.fst)) = _
+  have h_law : (𝔓).map (fun ω ↦ A n ω.1) = P.map (A n) := by
+    change ((𝔓).map (A n ∘ Prod.fst)) = _
     rw [← Measure.map_map (by fun_prop) (by fun_prop), ← Measure.fst, Measure.fst_prod]
   rw [h_law]
-  have h_prod : 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓']
+  have h_prod : 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓]
       =ᵐ[P.map (A n)] 𝓛[R n | A n; P] :=
     condDistrib_fst_prod _ (by fun_prop) _
   filter_upwards [h_ra', h_prod] with ω h_eq h_prod
@@ -64,13 +64,13 @@ lemma condDistrib_reward'' [Countable α]
 omit [DecidableEq α] in
 lemma reward_cond_action [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (n : ℕ)
-    (hμa : (𝔓').map (fun ω ↦ A n ω.1) {a} ≠ 0) :
-    𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1 ← a; 𝔓'] = ν a := by
+    (hμa : (𝔓).map (fun ω ↦ A n ω.1) {a} ≠ 0) :
+    𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1 ← a; 𝔓] = ν a := by
   have hA := h.measurable_A
   have hR := h.measurable_R
-  have h_ra : 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓'] =ᵐ[(𝔓').map (fun ω ↦ A n ω.1)] ν :=
+  have h_ra : 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓] =ᵐ[(𝔓).map (fun ω ↦ A n ω.1)] ν :=
     condDistrib_reward'' h n
-  have h_eq := condDistrib_ae_eq_cond (μ := 𝔓')
+  have h_eq := condDistrib_ae_eq_cond (μ := 𝔓)
     (X := fun ω ↦ A n ω.1) (Y := fun ω ↦ R n ω.1) (by fun_prop) (by fun_prop)
   rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq
   specialize h_ra a hμa
@@ -101,7 +101,7 @@ lemma condIndepFun_reward_stepsUntil_action [StandardBorelSpace Ω] [Countable 
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P)
     (a : α) (m n : ℕ) :
     CondIndepFun (mα.comap (fun ω ↦ A n ω.1)) ((h.measurable_A n).comp measurable_fst).comap_le
-      (fun ω ↦ R n ω.1) ({ω | stepsUntil A a m ω.1 = ↑n}.indicator (fun _ ↦ 1)) 𝔓' := by
+      (fun ω ↦ R n ω.1) ({ω | stepsUntil A a m ω.1 = ↑n}.indicator (fun _ ↦ 1)) 𝔓 := by
   have hA := h.measurable_A
   have hR := h.measurable_R
   exact condIndepFun_fst_prod (ν := streamMeasure ν)
@@ -110,37 +110,37 @@ lemma condIndepFun_reward_stepsUntil_action [StandardBorelSpace Ω] [Countable 
 
 lemma reward_cond_stepsUntil [StandardBorelSpace Ω] [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (m n : ℕ)
-    (hm : m ≠ 0) (hμn : 𝔓' ((fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n}) ≠ 0) :
-    𝓛[fun ω ↦ R n ω.1 | fun ω ↦ stepsUntil A a m ω.1 ← ↑n; 𝔓'] = ν a := by
+    (hm : m ≠ 0) (hμn : 𝔓 ((fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n}) ≠ 0) :
+    𝓛[fun ω ↦ R n ω.1 | fun ω ↦ stepsUntil A a m ω.1 ← ↑n; 𝔓] = ν a := by
   have hA := h.measurable_A
   have hR := h.measurable_R
   have hμna :
-      𝔓' ((fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ A n ω.1) ⁻¹' {a}) ≠ 0 := by
+      𝔓 ((fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ A n ω.1) ⁻¹' {a}) ≠ 0 := by
     suffices ((fun ω : Ω × (ℕ → α → ℝ) ↦
           stepsUntil A a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ A n ω.1) ⁻¹' {a})
         = (fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n} by simpa [this] using hμn
     ext ω
     simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, and_iff_left_iff_imp]
     exact action_eq_of_stepsUntil_eq_coe hm
-  have hμa : (𝔓').map (fun ω ↦ A n ω.1) {a} ≠ 0 := by
+  have hμa : (𝔓).map (fun ω ↦ A n ω.1) {a} ≠ 0 := by
     rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)]
     refine fun h_zero ↦ hμn (measure_mono_null (fun ω ↦ ?_) h_zero)
     simp only [Set.mem_preimage, Set.mem_singleton_iff]
     exact action_eq_of_stepsUntil_eq_coe hm
-  calc 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ stepsUntil A a m ω.1 ← (n : ℕ∞); 𝔓']
-  _ = (𝔓'[|(fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ A n ω.1) ⁻¹' {a}]).map
+  calc 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ stepsUntil A a m ω.1 ← (n : ℕ∞); 𝔓]
+  _ = (𝔓[|(fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ A n ω.1) ⁻¹' {a}]).map
       (fun ω ↦ R n ω.1) := by
     congr with ω
     simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and]
     exact action_eq_of_stepsUntil_eq_coe hm
-  _ = (𝔓'[|(fun ω ↦ A n ω.1) ⁻¹' {a}
+  _ = (𝔓[|(fun ω ↦ A n ω.1) ⁻¹' {a}
       ∩ {ω : Ω × (ℕ → α → ℝ) | stepsUntil A a m ω.1 = ↑n}.indicator 1 ⁻¹' {1} ]).map
       (fun ω ↦ R n ω.1) := by
     congr 2 with ω
     simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.indicator_apply,
       Set.mem_setOf_eq, Pi.one_apply, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
     rw [and_comm]
-  _ = 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1 ← a; 𝔓'] := by
+  _ = 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1 ← a; 𝔓] := by
     rw [cond_of_condIndepFun (by fun_prop)]
     · exact condIndepFun_reward_stepsUntil_action h a m n
     · refine measurable_one.indicator ?_
@@ -156,11 +156,11 @@ lemma reward_cond_stepsUntil [StandardBorelSpace Ω] [Countable α]
 given the time at which number of pulls is `m` is the constant kernel with value `ν a`. -/
 theorem condDistrib_rewardByCount_stepsUntil [StandardBorelSpace Ω] [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (m : ℕ) (hm : m ≠ 0) :
-    condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓'
-      =ᵐ[(𝔓').map (fun ω ↦ stepsUntil A a m ω.1)] Kernel.const _ (ν a) := by
+    condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓
+      =ᵐ[(𝔓).map (fun ω ↦ stepsUntil A a m ω.1)] Kernel.const _ (ν a) := by
   have hA := h.measurable_A
   have hR := h.measurable_R
-  refine (condDistrib_ae_eq_cond (μ := 𝔓')
+  refine (condDistrib_ae_eq_cond (μ := 𝔓)
     (X := fun ω ↦ stepsUntil A a m ω.1) (by fun_prop) (by fun_prop)).trans ?_
   rw [Filter.EventuallyEq, ae_iff_of_countable]
   intro n hn
@@ -189,44 +189,44 @@ theorem condDistrib_rewardByCount_stepsUntil [StandardBorelSpace Ω] [Countable
 /-- The reward received at the `m`-th pull of action `a` has law `ν a`. -/
 lemma hasLaw_rewardByCount [StandardBorelSpace Ω] [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (m : ℕ) (hm : m ≠ 0) :
-    HasLaw (rewardByCount A R a m) (ν a) 𝔓' where
+    HasLaw (rewardByCount A R a m) (ν a) 𝔓 where
   aemeasurable := (measurable_rewardByCount h.measurable_A h.measurable_R a m).aemeasurable
   map_eq := by
     have hA := h.measurable_A
     have hR := h.measurable_R
     have h_condDistrib :
-        condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓'
-        =ᵐ[(𝔓').map (fun ω ↦ stepsUntil A a m ω.1)]
+        condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓
+        =ᵐ[(𝔓).map (fun ω ↦ stepsUntil A a m ω.1)]
           Kernel.const _ (ν a) := condDistrib_rewardByCount_stepsUntil h a m hm
-    calc (𝔓').map (rewardByCount A R a m)
-    _ = (condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓')
-        ∘ₘ ((𝔓').map (fun ω ↦ stepsUntil A a m ω.1)) := by
+    calc (𝔓).map (rewardByCount A R a m)
+    _ = (condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓)
+        ∘ₘ ((𝔓).map (fun ω ↦ stepsUntil A a m ω.1)) := by
       rw [condDistrib_comp_map (by fun_prop) (by fun_prop)]
-    _ = (Kernel.const _ (ν a)) ∘ₘ ((𝔓').map (fun ω ↦ stepsUntil A a m ω.1)) :=
+    _ = (Kernel.const _ (ν a)) ∘ₘ ((𝔓).map (fun ω ↦ stepsUntil A a m ω.1)) :=
       Measure.comp_congr h_condDistrib
     _ = ν a := by
-      have : IsProbabilityMeasure ((𝔓').map (fun ω ↦ stepsUntil A a m ω.1)) :=
+      have : IsProbabilityMeasure ((𝔓).map (fun ω ↦ stepsUntil A a m ω.1)) :=
         Measure.isProbabilityMeasure_map (by fun_prop)
       simp
 
 lemma identDistrib_rewardByCount [StandardBorelSpace Ω] [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (n m : ℕ)
     (hn : n ≠ 0) (hm : m ≠ 0) :
-    IdentDistrib (rewardByCount A R a n) (rewardByCount A R a m) 𝔓' 𝔓' where
+    IdentDistrib (rewardByCount A R a n) (rewardByCount A R a m) 𝔓 𝔓 where
   aemeasurable_fst := (measurable_rewardByCount h.measurable_A h.measurable_R a n).aemeasurable
   aemeasurable_snd := (measurable_rewardByCount h.measurable_A h.measurable_R a m).aemeasurable
   map_eq := by rw [(hasLaw_rewardByCount h a n hn).map_eq, (hasLaw_rewardByCount h a m hm).map_eq]
 
 lemma identDistrib_rewardByCount_id [StandardBorelSpace Ω] [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (n : ℕ) (hn : n ≠ 0) :
-    IdentDistrib (rewardByCount A R a n) id 𝔓' (ν a) where
+    IdentDistrib (rewardByCount A R a n) id 𝔓 (ν a) where
   aemeasurable_fst := (measurable_rewardByCount h.measurable_A h.measurable_R a n).aemeasurable
   aemeasurable_snd := Measurable.aemeasurable <| by fun_prop
   map_eq := by rw [(hasLaw_rewardByCount h a n hn).map_eq, Measure.map_id]
 
 lemma identDistrib_rewardByCount_eval [StandardBorelSpace Ω] [Countable α]
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (n m : ℕ) (hn : n ≠ 0) :
-    IdentDistrib (rewardByCount A R a n) (fun ω ↦ ω m a) 𝔓' (streamMeasure ν) :=
+    IdentDistrib (rewardByCount A R a n) (fun ω ↦ ω m a) 𝔓 (streamMeasure ν) :=
   (identDistrib_rewardByCount_id h a n hn).trans
     (identDistrib_eval_eval_id_streamMeasure ν m a).symm
 
diff --git a/LeanBandits/Bandit/SumRewards.lean b/LeanBandits/Bandit/SumRewards.lean
index 8581224e..81ec80a3 100644
--- a/LeanBandits/Bandit/SumRewards.lean
+++ b/LeanBandits/Bandit/SumRewards.lean
@@ -13,34 +13,6 @@ import LeanBandits.ForMathlib.SubGaussian
 open MeasureTheory ProbabilityTheory Finset Learning
 open scoped ENNReal NNReal
 
-lemma measurable_sum_range_of_le {α : Type*} {mα : MeasurableSpace α}
-    {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ} (hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i))
-    (hg : Measurable g) :
-    Measurable (fun a ↦ ∑ i ∈ range (g a), f i a) := by
-  have h_eq : (fun a ↦ ∑ i ∈ range (g a), f i a)
-      = fun a ↦ ∑ i ∈ range (n + 1), if g a = i then ∑ j ∈ range i, f j a else 0 := by
-    ext ω
-    rw [sum_ite_eq_of_mem]
-    grind
-  rw [h_eq]
-  refine measurable_sum _ fun n hn ↦ ?_
-  refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
-  exact (measurableSet_singleton _).preimage (by fun_prop)
-
-lemma measurable_sum_Icc_of_le {α : Type*} {mα : MeasurableSpace α}
-    {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ} (hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i))
-    (hg : Measurable g) :
-    Measurable (fun a ↦ ∑ i ∈ Icc 1 (g a), f i a) := by
-  have h_eq : (fun a ↦ ∑ i ∈ Icc 1 (g a), f i a)
-      = fun a ↦ ∑ i ∈ range (n + 1), if g a = i then ∑ j ∈ Icc 1 i, f j a else 0 := by
-    ext ω
-    rw [sum_ite_eq_of_mem]
-    grind
-  rw [h_eq]
-  refine measurable_sum _ fun n hn ↦ ?_
-  refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
-  exact (measurableSet_singleton _).preimage (by fun_prop)
-
 namespace Bandits
 
 namespace ArrayModel
@@ -603,6 +575,60 @@ lemma prob_sum_ge_sqrt_log {σ2 : ℝ≥0}
       ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
     norm_cast
 
+open Real
+
+omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in
+lemma todo {σ2 : ℝ≥0} {c : ℝ}
+    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
+    (hc : 0 ≤ c) (a : α) (n k : ℕ) (hk : k ≠ 0) :
+    streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]} ≤
+      1 / (n + 1) ^ c := by
+  have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp)
+  calc
+    streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]}
+  _ = streamMeasure ν
+      {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) / k ≤ - √(2 * c * σ2 * log (n + 1) / k)} := by
+    congr with ω
+    field_simp
+    rw [Finset.sum_sub_distrib]
+    simp
+    grind
+  _ = streamMeasure ν
+      {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * log (n + 1))} := by
+    congr with ω
+    field_simp
+    congr! 2
+    rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt,
+      mul_assoc (k : ℝ), mul_assoc (k : ℝ), mul_assoc (k : ℝ),
+      sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm]
+  _ ≤ 1 / (n + 1) ^ c := prob_sum_le_sqrt_log hν hσ2 hc a k hk
+
+omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in
+lemma todo' {σ2 : ℝ≥0} {c : ℝ}
+    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
+    (hc : 0 ≤ c) (a : α) (n k : ℕ) (hk : k ≠ 0) :
+    streamMeasure ν
+        {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(2 * c * σ2 *log (n + 1) / k)} ≤
+      1 / (n + 1) ^ c := by
+  have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp)
+  calc
+    streamMeasure ν {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(2 * c * σ2 * log (n + 1) / k)}
+  _ = streamMeasure ν
+      {ω | √(2 * c * σ2 * log (n + 1) / k) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id])) / k} := by
+    congr with ω
+    field_simp
+    rw [Finset.sum_sub_distrib]
+    simp
+    grind
+  _ = streamMeasure ν
+      {ω | √(2 * c * k * σ2 * log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} := by
+    congr with ω
+    field_simp
+    congr! 1
+    rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt,
+      mul_comm _ (k : ℝ), sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm]
+  _ ≤ 1 / (n + 1) ^ c := prob_sum_ge_sqrt_log hν hσ2 hc a k hk
+
 end Subgaussian
 
 end Bandits
diff --git a/LeanBandits/BanditAlgorithms/AuxSums.lean b/LeanBandits/BanditAlgorithms/AuxSums.lean
index 27bdf41f..3ba38d6c 100644
--- a/LeanBandits/BanditAlgorithms/AuxSums.lean
+++ b/LeanBandits/BanditAlgorithms/AuxSums.lean
@@ -7,6 +7,11 @@ import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Tactic.Ring.RingNF
 
+/-!
+# Lemmas about sums of indicators
+
+-/
+
 open Finset
 
 lemma sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
diff --git a/LeanBandits/BanditAlgorithms/ETC.lean b/LeanBandits/BanditAlgorithms/ETC.lean
index b49c4f3a..93df488d 100644
--- a/LeanBandits/BanditAlgorithms/ETC.lean
+++ b/LeanBandits/BanditAlgorithms/ETC.lean
@@ -15,16 +15,6 @@ import LeanBandits.SequentialLearning.Deterministic
 open MeasureTheory ProbabilityTheory Finset Learning
 open scoped ENNReal NNReal
 
-section Aux
-
-lemma ae_eq_set_iff {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} {s t : Set α} :
-    s =ᵐ[μ] t ↔ ∀ᵐ a ∂μ, a ∈ s ↔ a ∈ t := by
-  rw [Filter.EventuallyEq]
-  simp only [eq_iff_iff]
-  congr!
-
-end Aux
-
 namespace Bandits
 
 variable {K : ℕ}
@@ -70,6 +60,8 @@ variable {hK : 0 < K} {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
   {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
   {σ2 : ℝ≥0}
 
+section AlgorithmBehavior
+
 lemma arm_zero [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
     A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := by
@@ -193,13 +185,15 @@ lemma sumRewards_bestArm_le_of_arm_mul_eq [Nonempty (Fin K)]
   · simp [ha, hm]
   · simp [h_best, hm]
 
+end AlgorithmBehavior
+
+section Regret
+
 lemma probReal_sumRewards_le_sumRewards_le [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K) :
     P.real {ω | sumRewards A R (bestArm ν) (K * m) ω ≤ sumRewards A R a (K * m) ω} ≤
       Real.exp (-↑m * gap ν a ^ 2 / (4 * σ2)) := by
-  have hA := h.measurable_A
-  have hR := h.measurable_R
   have h1 := Bandits.probReal_sumRewards_le_sumRewards_le h a (K * m) m m
   have h2 := probReal_sum_le_sum_streamMeasure hν a m
   refine le_trans (le_of_eq ?_) (h1.trans h2)
@@ -235,7 +229,6 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
     P[fun ω ↦ (pullCount A a n ω : ℝ)]
       ≤ m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2)) := by
   have hA := h.measurable_A
-  have hR := h.measurable_R
   have : (fun ω ↦ (pullCount A a n ω : ℝ))
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator (fun _ ↦ 1) ω := by
     filter_upwards [pullCount_of_ge h a hm hn] with ω h
@@ -263,16 +256,11 @@ lemma regret_le [Nonempty (Fin K)]
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hm : m ≠ 0)
     (n : ℕ) (hn : K * m ≤ n) :
     P[regret ν A n] ≤
-      ∑ a, gap ν a * (m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2))) := by
-  have hA := h.measurable_A
-  simp_rw [regret_eq_sum_pullCount_mul_gap]
-  rw [integral_finset_sum]
-  swap; · exact fun i _ ↦ (integrable_pullCount hA i n).mul_const _
-  gcongr with a
-  rw [mul_comm (gap _ _), integral_mul_const]
-  gcongr
-  · exact gap_nonneg
-  · exact expectation_pullCount_le h hν a hm hn
+      ∑ a, gap ν a * (m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2))) :=
+  integral_regret_le_of_forall_integral_pullCount_le h
+    (fun a _ ↦ expectation_pullCount_le h hν a hm hn)
+
+end Regret
 
 end ETC
 
diff --git a/LeanBandits/BanditAlgorithms/UCB.lean b/LeanBandits/BanditAlgorithms/UCB.lean
index 1aa5d1de..552389de 100644
--- a/LeanBandits/BanditAlgorithms/UCB.lean
+++ b/LeanBandits/BanditAlgorithms/UCB.lean
@@ -59,6 +59,8 @@ variable {hK : 0 < K} {c : ℝ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
   {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
   {σ2 : ℝ≥0} {n : ℕ} {ω : Ω}
 
+section AlgorithmBehavior
+
 /-- The exploration bonus of the UCB algorithm, which corresponds to the width of
 a confidence interval. -/
 noncomputable def ucbWidth (A : ℕ → Ω → Fin K) (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ :=
@@ -179,6 +181,8 @@ lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)]
   filter_upwards [time_gt_of_pullCount_gt_one h a, pullCount_pos_of_time_ge h] with ω h1 h2 n h_gt a
   exact h2 n (h1 n h_gt).le a
 
+end AlgorithmBehavior
+
 omit [IsMarkovKernel ν] in
 lemma gap_arm_le_two_mul_ucbWidth [Nonempty (Fin K)]
     (h_best : (ν (bestArm ν))[id] ≤ empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω)
@@ -215,54 +219,6 @@ lemma pullCount_arm_le [Nonempty (Fin K)] (hc : 0 ≤ c)
   · have : 0 ≤ log (n + 1) := by simp [log_nonneg]
     positivity
 
-lemma todo (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
-    (hc : 0 ≤ c) (a : Fin K) (n k : ℕ) (hk : k ≠ 0) :
-    streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]} ≤
-      1 / (n + 1) ^ c := by
-  have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp)
-  calc
-    streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]}
-  _ = streamMeasure ν
-      {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) / k ≤ - √(2 * c * σ2 * log (n + 1) / k)} := by
-    congr with ω
-    field_simp
-    rw [Finset.sum_sub_distrib]
-    simp
-    grind
-  _ = streamMeasure ν
-      {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * log (n + 1))} := by
-    congr with ω
-    field_simp
-    congr! 2
-    rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt,
-      mul_assoc (k : ℝ), mul_assoc (k : ℝ), mul_assoc (k : ℝ),
-      sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm]
-  _ ≤ 1 / (n + 1) ^ c := prob_sum_le_sqrt_log hν hσ2 hc a k hk
-
-lemma todo' (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
-    (hc : 0 ≤ c) (a : Fin K) (n k : ℕ) (hk : k ≠ 0) :
-    streamMeasure ν
-        {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(2 * c * σ2 *log (n + 1) / k)} ≤
-      1 / (n + 1) ^ c := by
-  have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp)
-  calc
-    streamMeasure ν {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(2 * c * σ2 * log (n + 1) / k)}
-  _ = streamMeasure ν
-      {ω | √(2 * c * σ2 * log (n + 1) / k) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id])) / k} := by
-    congr with ω
-    field_simp
-    rw [Finset.sum_sub_distrib]
-    simp
-    grind
-  _ = streamMeasure ν
-      {ω | √(2 * c * k * σ2 * log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} := by
-    congr with ω
-    field_simp
-    congr! 1
-    rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt,
-      mul_comm _ (k : ℝ), sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm]
-  _ ≤ 1 / (n + 1) ^ c := prob_sum_ge_sqrt_log hν hσ2 hc a k hk
-
 -- todo: this is not about UCB but about any algorithm with subgaussian rewards. Move it?
 lemma prob_ucbIndex_le [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P)
@@ -628,19 +584,13 @@ lemma regret_le [Nonempty (Fin K)]
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) :
     P[regret ν A n] ≤
       ∑ a, (8 * c * σ2 * log (n + 1) / gap ν a + gap ν a * (2 + 2 * (constSum c n).toReal)) := by
-  have hA := h.measurable_A
-  simp_rw [regret_eq_sum_pullCount_mul_gap]
-  rw [integral_finset_sum]
-  swap; · exact fun i _ ↦ (integrable_pullCount hA i n).mul_const _
-  gcongr with a
-  rw [integral_mul_const]
+  refine (integral_regret_le_of_forall_integral_pullCount_le h
+    (fun a h_gap ↦ expectation_pullCount_le h hν hσ2 hc a
+      (lt_of_le_of_ne' gap_nonneg h_gap) n)).trans_eq ?_
+  congr with a
   by_cases h_gap : gap ν a = 0
   · simp [h_gap]
-  replace h_gap : 0 < gap ν a := lt_of_le_of_ne gap_nonneg (Ne.symm h_gap)
-  grw [expectation_pullCount_le h hν hσ2 hc a h_gap n]
-  refine le_of_eq ?_
-  rw [mul_add]
-  field
+  · field
 
 end UCB
 
diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean
index 030e1bd6..2ce5cfb3 100644
--- a/LeanBandits/ForMathlib/CondDistrib.lean
+++ b/LeanBandits/ForMathlib/CondDistrib.lean
@@ -18,62 +18,8 @@ variable {α β γ δ Ω Ω' : Type*}
   [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω'] [Nonempty Ω']
   {X : α → β} {Y : α → Ω} {Z : α → Ω'} {T : α → γ}
 
-lemma ae_map_iff_ae_trim {f : α → β} (hf : Measurable f) {p : β → Prop}
-    (hp : MeasurableSet { x | p x }) :
-    (∀ᵐ y ∂μ.map f, p y) ↔ ∀ᵐ x ∂(μ.trim hf.comap_le), p (f x) := by
-  rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]
-
-@[fun_prop]
-lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) :
-    Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf
-
-@[fun_prop]
-lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat) :=
-  Measurable.comp (by fun_prop) hf
-
-namespace MeasureTheory.Measure
-
-lemma trim_comap_apply (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) :
-    μ.trim hX.comap_le (X ⁻¹' s) = μ.map X s := by
-  rw [trim_measurableSet_eq, Measure.map_apply (by fun_prop) hs]
-  exact ⟨s, hs, rfl⟩
-
-end MeasureTheory.Measure
-
 namespace ProbabilityTheory
 
-section IndepFun
-
-lemma Kernel.IndepFun.of_prod_right {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
-    {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
-    (h : IndepFun X (fun ω ↦ (Y ω, T ω)) κ μ) :
-    IndepFun X Y κ μ := by
-  rw [Kernel.indepFun_iff_measure_inter_preimage_eq_mul] at h ⊢
-  intro s t hs ht
-  specialize h s (t ×ˢ .univ) hs (ht.prod .univ)
-  simpa [Set.mk_preimage_prod] using h
-
-lemma Kernel.IndepFun.of_prod_left {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
-    {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
-    (h : IndepFun (fun ω ↦ (X ω, T ω)) Y κ μ) :
-    IndepFun X Y κ μ := h.symm.of_prod_right.symm
-
-lemma CondIndepFun.of_prod_right {ε : Type*} {mε : MeasurableSpace ε}
-    [StandardBorelSpace α] [IsFiniteMeasure μ]
-    {X : α → β} {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
-    (h : X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, T ω))) :
-    X ⟂ᵢ[Z, hZ; μ] Y :=
-  Kernel.IndepFun.of_prod_right h
-
-lemma CondIndepFun.of_prod_left {ε : Type*} {mε : MeasurableSpace ε}
-    [StandardBorelSpace α] [IsFiniteMeasure μ]
-    {X : α → β} {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
-    (h : (fun ω ↦ (X ω, T ω)) ⟂ᵢ[Z, hZ; μ] Y) :
-    X ⟂ᵢ[Z, hZ; μ] Y :=
-  Kernel.IndepFun.of_prod_left h
-
-end IndepFun
-
 section CondDistrib
 
 variable [IsFiniteMeasure μ]
diff --git a/LeanBandits/ForMathlib/CondIndepFun.lean b/LeanBandits/ForMathlib/CondIndepFun.lean
index d361705a..ee7efa2b 100644
--- a/LeanBandits/ForMathlib/CondIndepFun.lean
+++ b/LeanBandits/ForMathlib/CondIndepFun.lean
@@ -22,6 +22,34 @@ variable {α β γ δ γ' δ' : Type*}
   {μ : Measure α}
   {X : α → β} {hX : Measurable X} {Y : α → γ} {Z : α → δ} {Y' : α → γ'} {Z' : α → δ'}
 
+lemma Kernel.IndepFun.of_prod_right {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
+    {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
+    (h : IndepFun X (fun ω ↦ (Y ω, T ω)) κ μ) :
+    IndepFun X Y κ μ := by
+  rw [Kernel.indepFun_iff_measure_inter_preimage_eq_mul] at h ⊢
+  intro s t hs ht
+  specialize h s (t ×ˢ .univ) hs (ht.prod .univ)
+  simpa [Set.mk_preimage_prod] using h
+
+lemma Kernel.IndepFun.of_prod_left {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
+    {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
+    (h : IndepFun (fun ω ↦ (X ω, T ω)) Y κ μ) :
+    IndepFun X Y κ μ := h.symm.of_prod_right.symm
+
+lemma CondIndepFun.of_prod_right {ε : Type*} {mε : MeasurableSpace ε}
+    [StandardBorelSpace α] [IsFiniteMeasure μ]
+    {X : α → β} {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
+    (h : X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, T ω))) :
+    X ⟂ᵢ[Z, hZ; μ] Y :=
+  Kernel.IndepFun.of_prod_right h
+
+lemma CondIndepFun.of_prod_left {ε : Type*} {mε : MeasurableSpace ε}
+    [StandardBorelSpace α] [IsFiniteMeasure μ]
+    {X : α → β} {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
+    (h : (fun ω ↦ (X ω, T ω)) ⟂ᵢ[Z, hZ; μ] Y) :
+    X ⟂ᵢ[Z, hZ; μ] Y :=
+  Kernel.IndepFun.of_prod_left h
+
 lemma IndepFun.of_measurable (h_indep : Y ⟂ᵢ[μ] Z)
     (hY_meas : Measurable[mγ.comap Y] Y') (hZ_meas : Measurable[mδ.comap Z] Z') :
     Y' ⟂ᵢ[μ] Z' := by
diff --git a/LeanBandits/ForMathlib/Integrable.lean b/LeanBandits/ForMathlib/Integrable.lean
new file mode 100644
index 00000000..8feeb38f
--- /dev/null
+++ b/LeanBandits/ForMathlib/Integrable.lean
@@ -0,0 +1,22 @@
+/-
+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
+-/
+import Mathlib
+
+open ProbabilityTheory
+
+namespace MeasureTheory
+
+lemma Integrable.congr_identDistrib {Ω Ω' : Type*}
+    {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
+    {μ : Measure Ω} {μ' : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ}
+    (hX : Integrable X μ) (hXY : IdentDistrib X Y μ μ') :
+    Integrable Y μ' := by
+  have hX' : Integrable id (μ.map X) := by
+    rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_fst]
+  rw [hXY.map_eq] at hX'
+  rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_snd] at hX'
+
+end MeasureTheory
diff --git a/LeanBandits/ForMathlib/Measurable.lean b/LeanBandits/ForMathlib/Measurable.lean
index 3f907ce9..5a36cdb4 100644
--- a/LeanBandits/ForMathlib/Measurable.lean
+++ b/LeanBandits/ForMathlib/Measurable.lean
@@ -3,23 +3,33 @@ 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
 -/
-import Mathlib.MeasureTheory.MeasurableSpace.Basic
+import Mathlib.Analysis.Normed.Ring.Basic
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
 
 /-!
 # Measurability lemmas
 -/
 
+open Finset
+
 namespace MeasureTheory
 
-lemma measurable_comp_comap {α β γ : Type*} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
-    (f : α → β) {g : β → γ} (hg : Measurable g) :
+variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+  {μ : Measure α}
+
+lemma ae_eq_set_iff {s t : Set α} : s =ᵐ[μ] t ↔ ∀ᵐ a ∂μ, a ∈ s ↔ a ∈ t := by
+  rw [Filter.EventuallyEq]
+  simp only [eq_iff_iff]
+  congr!
+
+lemma measurable_comp_comap (f : α → β) {g : β → γ} (hg : Measurable g) :
     Measurable[mβ.comap f] (g ∘ f) := by
   rw [measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
   refine MeasurableSpace.comap_mono ?_
   rw [← measurable_iff_comap_le]
   exact hg
 
-lemma MeasurableSet.imp {α : Type*} {mα : MeasurableSpace α} {p q : α → Prop}
+lemma MeasurableSet.imp {p q : α → Prop}
     (hs : MeasurableSet {x | p x}) (ht : MeasurableSet {x | q x}) :
     MeasurableSet {x | p x → q x} := by
   have h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x} := by
@@ -28,7 +38,7 @@ lemma MeasurableSet.imp {α : Type*} {mα : MeasurableSpace α} {p q : α → Pr
   rw [h_eq]
   exact MeasurableSet.union hs.compl ht
 
-lemma MeasurableSet.iff {α : Type*} {mα : MeasurableSpace α} {p q : α → Prop}
+lemma MeasurableSet.iff {p q : α → Prop}
     (hs : MeasurableSet {x | p x}) (ht : MeasurableSet {x | q x}) :
     MeasurableSet {x | p x ↔ q x} := by
   have h_eq : {x | p x ↔ q x} = ({x | p x}ᶜ ∪ {x | q x}) ∩ ({x | q x}ᶜ ∪ {x | p x}) := by
@@ -38,4 +48,43 @@ lemma MeasurableSet.iff {α : Type*} {mα : MeasurableSpace α} {p q : α → Pr
   rw [h_eq]
   exact (MeasurableSet.union hs.compl ht).inter (MeasurableSet.union ht.compl hs)
 
+@[fun_prop]
+lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) :
+    Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf
+
+@[fun_prop]
+lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat) :=
+  Measurable.comp (by fun_prop) hf
+
+lemma Measure.trim_comap_apply {X : α → β} (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) :
+    μ.trim hX.comap_le (X ⁻¹' s) = μ.map X s := by
+  rw [trim_measurableSet_eq, Measure.map_apply (by fun_prop) hs]
+  exact ⟨s, hs, rfl⟩
+
+lemma measurable_sum_range_of_le {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
+    (hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i)) (hg : Measurable g) :
+    Measurable (fun a ↦ ∑ i ∈ range (g a), f i a) := by
+  have h_eq : (fun a ↦ ∑ i ∈ range (g a), f i a)
+      = fun a ↦ ∑ i ∈ range (n + 1), if g a = i then ∑ j ∈ range i, f j a else 0 := by
+    ext ω
+    rw [sum_ite_eq_of_mem]
+    grind
+  rw [h_eq]
+  refine measurable_sum _ fun n hn ↦ ?_
+  refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
+  exact (measurableSet_singleton _).preimage (by fun_prop)
+
+lemma measurable_sum_Icc_of_le {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
+    (hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i)) (hg : Measurable g) :
+    Measurable (fun a ↦ ∑ i ∈ Icc 1 (g a), f i a) := by
+  have h_eq : (fun a ↦ ∑ i ∈ Icc 1 (g a), f i a)
+      = fun a ↦ ∑ i ∈ range (n + 1), if g a = i then ∑ j ∈ Icc 1 i, f j a else 0 := by
+    ext ω
+    rw [sum_ite_eq_of_mem]
+    grind
+  rw [h_eq]
+  refine measurable_sum _ fun n hn ↦ ?_
+  refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
+  exact (measurableSet_singleton _).preimage (by fun_prop)
+
 end MeasureTheory
diff --git a/LeanBandits/SequentialLearning/Algorithm.lean b/LeanBandits/SequentialLearning/Algorithm.lean
index df3c528b..a35d68a9 100644
--- a/LeanBandits/SequentialLearning/Algorithm.lean
+++ b/LeanBandits/SequentialLearning/Algorithm.lean
@@ -234,6 +234,8 @@ theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
     exact h.hasLaw_step_zero
   · exact h.hasCondDistrib_step n
 
+/-- The law of the sequence of actions and observations generated by an algorithm-environment pair
+is unique: it does not depend on the probability space used. -/
 theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
     (h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
     P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index ce50c4fb..003554c0 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -93,6 +93,7 @@ Bandits.regret
 Bandits.gap
 Learning.sum_pullCount_mul
 Bandits.regret_eq_sum_pullCount_mul_gap
+Bandits.integral_regret_eq_sum_gap_mul_integral_pullCount
 ProbabilityTheory.HasSubgaussianMGF
 ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
 ProbabilityTheory.HasSubgaussianMGF.measure_ge_le
diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex
index 13552567..a538a3aa 100644
--- a/blueprint/src/chapters/algorithm.tex
+++ b/blueprint/src/chapters/algorithm.tex
@@ -72,8 +72,14 @@ \chapter{Iterative stochastic algorithms}
 For example, we may want to prove that an optimization algorithm converges to the minimum of a function almost surely.
 For such a statement to make sense, we need a probability space on which the whole sequence of actions and observations is defined as a random variable.
 
-We denote by $P[X \mid Y]$ the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$.
-When we write that $P[X \mid Y] = \kappa$, or that $X$ has conditional distribution $\kappa$ given $Y$, the equality should be understood as holding $Y_* P$-almost surely.
+We denote by $P(X \mid Y)$ the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$.
+When we write that $P(X \mid Y) = \kappa$, or that $X$ has conditional distribution $\kappa$ given $Y$, the equality should be understood as holding $Y_* P$-almost surely.
+
+
+\begin{remark}[Lean remark: \texttt{HasCondDistrib}]
+In the Lean implementation, we define a predicate to state those almost sure equalities of conditional distributions: \texttt{HasCondDistrib X Y k P} states that under the probability measure $P$, the random variable $X$ has conditional distribution $k$ given the random variable $Y$ (almost surely with respect to the law of $X$).
+For convenience, the predicate also records that both random variables are almost everywhere measurable.
+\end{remark}
 
 
 \begin{definition}[Algorithm-environment interaction]\label{def:IsAlgEnvSeq}
@@ -84,9 +90,9 @@ \chapter{Iterative stochastic algorithms}
 A probability space $(\Omega, P)$ and two sequences of random variables $A : \mathbb{N} \to \Omega \to \mathcal{A}$ and $R : \mathbb{N} \to \Omega \to \mathcal{R}$ form an algorithm-environment interaction for $\mathfrak{A}$ and $\mathfrak{E}$ if the following conditions hold:
 \begin{enumerate}
   \item The law of $A_0$ is $P_0$.
-  \item $P \left[ R_0 \mid A_0 \right] = \nu'_0$.
-  \item For all $t \in \mathbb{N}$, $P\left[A_{t+1} \mid A_0, R_0, \ldots, A_t, R_t \right] = \pi_t$.
-  \item For all $t \in \mathbb{N}$, $P\left[R_{t+1} \mid A_0, R_0, \ldots, A_t, R_t, A_{t+1}\right] = \nu_t$.
+  \item $P \left( R_0 \mid A_0 \right) = \nu'_0$.
+  \item For all $t \in \mathbb{N}$, $P\left(A_{t+1} \mid A_0, R_0, \ldots, A_t, R_t \right) = \pi_t$.
+  \item For all $t \in \mathbb{N}$, $P\left(R_{t+1} \mid A_0, R_0, \ldots, A_t, R_t, A_{t+1}\right) = \nu_t$.
 \end{enumerate}
 \end{definition}
 
@@ -106,7 +112,7 @@ \chapter{Iterative stochastic algorithms}
 In an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq},
 \begin{itemize}
   \item the law of the initial step $X_0$ is $P_0 \otimes \nu'_0$,
-  \item for all $t \in \mathbb{N}$, $P \left[ X_{t+1} \mid H_t \right] = \pi_t \otimes \nu_t$.
+  \item for all $t \in \mathbb{N}$, $P \left( X_{t+1} \mid H_t \right) = \pi_t \otimes \nu_t$.
 \end{itemize}
 \end{lemma}
 
@@ -148,7 +154,7 @@ \section{Stationary environment}
   \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm}
   \leanok
   \lean{Learning.IsAlgEnvSeq.condDistrib_reward_stationaryEnv}
-In a stationary environment, for any $t \in \mathbb{N}$, the conditional distribution $P\left[R_t \mid A_t\right]$ is $(A_{t*} P_{\mathcal{T}})$-almost surely equal to $\nu$.
+In a stationary environment, for any $t \in \mathbb{N}$, $P\left(R_t \mid A_t\right) = \nu$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -248,7 +254,7 @@ \subsection{Ionescu-Tulcea theorem}
   \uses{def:IT.history, thm:ionescu-tulcea, def:trajMeasure}
   \leanok
   \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure}
-For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$.
+For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -308,13 +314,13 @@ \subsection{Case of an algorithm-environment interaction}
   \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history}
   \leanok
   \lean{Learning.IT.condDistrib_action}
-For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right] = \pi_t$.
+For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right) = \pi_t$.
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{lem:IT.condDistrib_X_add_one,def:IT.history}
-By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right] = \kappa_t = \pi_t \otimes \nu_t$.
-Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}$, $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to the projection of $\kappa_t$ on $\mathcal{A}$, which is $\pi_t$.
+By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t = \pi_t \otimes \nu_t$.
+Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}$, $P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right)$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to the projection of $\kappa_t$ on $\mathcal{A}$, which is $\pi_t$.
 \end{proof}
 
 
@@ -322,13 +328,13 @@ \subsection{Case of an algorithm-environment interaction}
   \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history}
   \leanok
   \lean{Learning.IT.condDistrib_reward}
-For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right] = \nu_t$.
+For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left(R_{t+1} \mid H_t, A_{t+1}\right) = \nu_t$.
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{lem:IT.condDistrib_X_add_one,def:IT.history,lem:IT.condDistrib_A_add_one}
 It suffices to show that $((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t = (H_t, A_{t+1}, R_{t+1})_* P_{\mathcal{T}} = (H_t, X_{t+1})_* P_{\mathcal{T}}$.
-By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right] = \pi_t \otimes \nu_t$.
+By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \pi_t \otimes \nu_t$.
 Thus $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = (H_t, X_{t+1})_* P_{\mathcal{T}}$.
 
 We thus have to prove that $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = ((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t$.
@@ -354,13 +360,13 @@ \subsection{Case of an algorithm-environment interaction}
   \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure}
   \leanok
   \lean{Learning.IT.condDistrib_reward_zero}
-$P_{\mathcal{T}}\left[R_0 \mid A_0\right] = \nu'_0$.
+$P_{\mathcal{T}}\left(R_0 \mid A_0\right) = \nu'_0$.
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{lem:IT.law_X_zero,lem:IT.law_A_zero,def:IT.history}
-To prove almost sure equality, it is enough to prove that $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left[R_0 \mid A_0\right] = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0$.
-By definition of the conditional distribution, we have $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left[R_0 \mid A_0\right] = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}$.
+To prove almost sure equality, it is enough to prove that $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0$.
+By definition of the conditional distribution, we have $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}$.
 By Lemma~\ref{lem:IT.law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = P_0 \otimes \nu'_0$.
 By Lemma~\ref{lem:IT.law_A_zero}, $A_{0*} P_{\mathcal{T}} = P_0$.
 Thus the two sides are equal.
diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex
index 68f7ff9d..ce0f10c4 100644
--- a/blueprint/src/chapters/bandit.tex
+++ b/blueprint/src/chapters/bandit.tex
@@ -327,7 +327,7 @@ \subsection{Laws}
   \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea}
   \leanok
   \lean{Bandits.ArrayModel.hasCondDistrib_reward_zero}
-In the array model, $P_{\mathcal{A}}[R_0 \mid A_0] = \nu$.
+In the array model, $P_{\mathcal{A}}(R_0 \mid A_0) = \nu$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -340,7 +340,7 @@ \subsection{Laws}
   \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea}
   \leanok
   \lean{Bandits.ArrayModel.hasCondDistrib_action}
-In the array model, $P_{\mathcal{A}}[A_{t+1} \mid H_t] = \pi_t$.
+In the array model, $P_{\mathcal{A}}(A_{t+1} \mid H_t) = \pi_t$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -353,7 +353,7 @@ \subsection{Laws}
   \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:pullCount}
 \leanok
   \lean{Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action}
-In the array model, $P_{\mathcal{A}}[R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}] = \nu$.
+In the array model, $P_{\mathcal{A}}(R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}) = \nu$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -366,7 +366,7 @@ \subsection{Laws}
   \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:pullCount}
 \leanok
   \lean{Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount}
-In the array model, $P_{\mathcal{A}}[R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}] = \nu$.
+In the array model, $P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}) = \nu$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -392,7 +392,7 @@ \subsection{Laws}
   \uses{def:arrayMeasure,def:AM.history,def:stationaryEnv,def:environment,def:algorithm,thm:ionescu-tulcea}
   \leanok
   \lean{Bandits.ArrayModel.hasCondDistrib_reward}
-In the array model, $P_{\mathcal{A}}[R_{t+1} \mid H_t, A_{t+1}] = \nu$.
+In the array model, $P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}) = \nu$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -456,17 +456,17 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model}
   \leanok
   \lean{Bandits.reward_cond_stepsUntil}
 Let $n > 0$, $t \in \mathbb{N}$ and suppose that $P(T_{n, a} = t) > 0$.
-Then $\mathcal{L}(R_t \mid T_{n, a} = t) = \nu(a)$.
+Then $P(R_t \mid T_{n, a} = t) = \nu(a)$.
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{def:environment,lem:stepsUntil_basic,lem:condIndepFun_reward_stepsUntil_arm,def:pullCount,lem:condDistrib_ae_eq_cond,lem:condDistrib_reward_stationaryEnv}
-First, if $T_{n, a} = t$, then $A_t = a$ (Lemma~\ref{lem:stepsUntil_basic}), such that $\mathcal{L}(R_t \mid T_{n, a} = t) = \mathcal{L}(R_t \mid T_{n, a} = t, A_t = a)$.
+First, if $T_{n, a} = t$, then $A_t = a$ (Lemma~\ref{lem:stepsUntil_basic}), such that $P(R_t \mid T_{n, a} = t) = P(R_t \mid T_{n, a} = t, A_t = a)$.
 
 Then, using first the independence from Lemma~\ref{lem:condIndepFun_reward_stepsUntil_arm} and then the conditional distribution from Lemma~\ref{lem:condDistrib_reward_stationaryEnv}, we have
 \begin{align*}
-  \mathcal{L}(R_t \mid T_{n, a} = t, A_t = a)
-  &= \mathcal{L}(R_t \mid A_t = a)
+  P(R_t \mid T_{n, a} = t, A_t = a)
+  &= P(R_t \mid A_t = a)
   = \nu(a)
   \: .
 \end{align*}
@@ -476,8 +476,8 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model}
 \begin{lemma}\label{lem:condDistrib_ae_eq_cond}
   \leanok
   \lean{ProbabilityTheory.condDistrib_ae_eq_cond}
-For a random variable $X$ on a countable space with the discrete sigma algebra, $\mathcal{L}(Y \mid X) = (x \mapsto \mathcal{L}(Y \mid X = x))$, $(X_*P)$-almost surely.
-Furthermore, that almost sure equality means that for all $x$ such that $P(X = x) > 0$, we have $\mathcal{L}(Y \mid X = x) = \mathcal{L}(Y \mid X)(x)$.
+For a random variable $X$ on a countable space with the discrete sigma algebra, $P(Y \mid X) = (x \mapsto P(Y \mid X = x))$, $(X_*P)$-almost surely.
+Furthermore, that almost sure equality means that for all $x$ such that $P(X = x) > 0$, we have $P(Y \mid X = x) = P(Y \mid X)(x)$.
 \end{lemma}
 
 \begin{proof}\leanok
@@ -489,16 +489,16 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model}
   \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:rewardByCount,def:stepsUntil}
 \leanok
   \lean{Bandits.condDistrib_rewardByCount_stepsUntil}
-For $n > 0$ and $t \in \mathbb{N}$, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$ (in which the measure on the r.h.s. is seen as a constant kernel).
+For $n > 0$ and $t \in \mathbb{N}$, $P(Y_{n,a} \mid T_{n,a}) = \nu(a)$ (in which the measure on the r.h.s. is seen as a constant kernel).
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{def:environment,lem:reward_cond_stepsUntil,def:pullCount,lem:condDistrib_ae_eq_cond}
-It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$ such that $\mathbb{P}(T_{n, a} = t) > 0$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$.
+It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$ such that $P(T_{n, a} = t) > 0$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$.
 
-If $t < \infty$, then $\mathcal{L}(Y_{n, a} \mid T_{n, a} = t) = \mathcal{L}(R_t \mid T_{n, a} = t) = \nu(a)$ by Lemma~\ref{lem:reward_cond_stepsUntil}.
+If $t < \infty$, then $P(Y_{n, a} \mid T_{n, a} = t) = P(R_t \mid T_{n, a} = t) = \nu(a)$ by Lemma~\ref{lem:reward_cond_stepsUntil}.
 
-If $t = \infty$, then $\mathcal{L}(Y_{n, a} \mid T_{n, a} = \infty) = \mathcal{L}(Z_{n, a} \mid T_{n, a} = \infty)$. By independence of $Z_{n,a}$ and $T_{n, a}$, this is just $\nu(a)$, the law of $Z_{n,a}$.
+If $t = \infty$, then $P(Y_{n, a} \mid T_{n, a} = \infty) = P(Z_{n, a} \mid T_{n, a} = \infty)$. By independence of $Z_{n,a}$ and $T_{n, a}$, this is just $\nu(a)$, the law of $Z_{n,a}$.
 \end{proof}
 
 
@@ -506,13 +506,13 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model}
   \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:rewardByCount}
   \leanok
   \lean{Bandits.hasLaw_rewardByCount}
-For $n > 0$ and $a \in \mathcal{A}$, $\mathcal{L}(Y_{n,a}) = \nu(a)$.
+For $n > 0$ and $a \in \mathcal{A}$, $(Y_{n,a})_*P = \nu(a)$.
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{def:environment,lem:condDistrib_rewardByCount_stepsUntil,def:stepsUntil,def:pullCount}
-The law of $Y_{n,a}$ is given by $\mathcal{L}(Y_{n, a}) = \mathcal{L}(Y_{n, a} \mid T_{n, a}) \circ \mathcal{L}(T_{n, a})$.
-By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n, a} \mid T_{n, a}) = \nu(a)$, a constant kernel.
+The law of $Y_{n,a}$ is given by $(Y_{n, a})_*P = P(Y_{n, a} \mid T_{n, a}) \circ (T_{n, a})_*P$.
+By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $P(Y_{n, a} \mid T_{n, a}) = \nu(a)$, a constant kernel.
 Thus the composition is just $\nu(a)$.
 \end{proof}
 
@@ -649,6 +649,7 @@ \section{Regret and other bandit quantities}
 \end{align*}
 \end{definition}
 
+TODO: the $R_T$ notation clashes with the random variable $R_t$.
 
 \begin{definition}\label{def:gap}
   \uses{def:armMean}
@@ -704,3 +705,19 @@ \section{Regret and other bandit quantities}
   \: .
 \end{align*}
 \end{proof}
+
+
+\begin{corollary}\label{cor:integral_regret_eq_sum_mul}
+  \uses{def:regret,def:gap,def:pullCount}
+  \leanok
+  \lean{Bandits.integral_regret_eq_sum_gap_mul_integral_pullCount}
+For $\mathcal{A}$ finite, the expected regret can be expressed as a sum over the arms and their gaps:
+\begin{align*}
+  P[R_T] = \sum_{a \in \mathcal{A}}P[N_{T,a}] \Delta_a \: .
+\end{align*}
+\end{corollary}
+
+\begin{proof}\leanok
+  \uses{lem:regret_eq_sum_pullCount_mul_gap}
+
+\end{proof}
diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex
index e4e94c6c..5a888471 100644
--- a/blueprint/src/chapters/concentration.tex
+++ b/blueprint/src/chapters/concentration.tex
@@ -8,7 +8,7 @@ \section{Sub-Gaussian random variables}
   \lean{ProbabilityTheory.HasSubgaussianMGF}
 A real valued random variable $X$ is $\sigma^2$-sub-Gaussian if for any $\lambda \in \mathbb{R}$,
 \begin{align*}
-  \mathbb{E}\left[e^{\lambda X}\right]
+  P\left[e^{\lambda X}\right]
   &\le e^{\frac{\lambda^2 \sigma^2}{2}}
   \: .
 \end{align*}
@@ -33,7 +33,7 @@ \section{Sub-Gaussian random variables}
   \lean{ProbabilityTheory.HasSubgaussianMGF.measure_ge_le}
 For $X$ a $\sigma^2$-sub-Gaussian random variable, for any $t \ge 0$,
 \begin{align*}
-  \mathbb{P}(X \ge t)
+  P(X \ge t)
   &\le \exp\left(- \frac{t^2}{2 \sigma^2}\right)
   \: .
 \end{align*}
@@ -51,7 +51,7 @@ \section{Sub-Gaussian random variables}
 Let $X_1, \ldots, X_n$ be independent random variables such that $X_i$ is $\sigma_i^2$-sub-Gaussian for $i \in [n]$.
 Then for any $t \ge 0$,
 \begin{align*}
-  \mathbb{P}\left(\sum_{i=1}^n X_i \ge t\right)
+  P\left(\sum_{i=1}^n X_i \ge t\right)
   &\le \exp\left(- \frac{t^2}{2 \sum_{i=1}^n \sigma_i^2}\right)
   \: .
 \end{align*}
@@ -72,7 +72,7 @@ \section{Sub-Gaussian random variables}
 Suppose further that the vectors $X$ and $Y$ are independent and that $\sum_{i = 1}^m P[Y_i] \le \sum_{i = 1}^n P[X_i]$.
 Then
 \begin{align*}
-  \mathbb{P}\left(\sum_{i=1}^m Y_i \ge \sum_{i=1}^n X_i\right)
+  P\left(\sum_{i=1}^m Y_i \ge \sum_{i=1}^n X_i\right)
   &\le \exp\left(- \frac{\left(\sum_{i = 1}^n P[X_i] - \sum_{i=1}^m P[Y_i]\right)^2}{2 \sum_{i=1}^n (\sigma_{X,i}^2 + \sigma_{Y,i}^2)}\right)
   \: .
 \end{align*}
diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex
index 0dc2c829..7bec9e10 100644
--- a/blueprint/src/chapters/etc.tex
+++ b/blueprint/src/chapters/etc.tex
@@ -55,20 +55,20 @@ \section{Explore-Then-Commit}
   \leanok
   \lean{Bandits.ETC.prob_arm_mul_eq_le}
 Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$.
-Then for the Explore-Then-Commit algorithm with parameter $m$, for any arm $a \in [K]$ with $\Delta_a > 0$, we have $\mathbb{P}(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)$.
+Then for the Explore-Then-Commit algorithm with parameter $m$, for any arm $a \in [K]$ with $\Delta_a > 0$, we have $P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)$.
 \end{lemma}
 
 \begin{proof}\leanok
   \uses{def:environment,lem:probReal_sum_le_sum_streamMeasure,lem:prob_sumRewards_le_sumRewards_le,def:detAlgorithm,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:history,lem:sumRewards_bestArm_le_of_arm_mul_eq,def:pullCount,def:etcAlgorithm}
 By Lemma~\ref{lem:sumRewards_bestArm_le_of_arm_mul_eq},
 \begin{align*}
-  \mathbb{P}(\hat{A}_m^* = a)
-  &\le \mathbb{P}(S_{Km, a} \ge S_{Km, a^*})
+  P(\hat{A}_m^* = a)
+  &\le P(S_{Km, a} \ge S_{Km, a^*})
   \: .
 \end{align*}
 By Lemma~\ref{lem:prob_sumRewards_le_sumRewards_le}, and then the concentration inequality of Lemma~\ref{lem:probReal_sum_le_sum_streamMeasure} we have
 \begin{align*}
-  P_{\mathcal{A}}\left(S_{Km, a^*} \le S_{Km, a}\right)
+  P\left(S_{Km, a^*} \le S_{Km, a}\right)
   &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right)
   \\
   &\le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right)
@@ -84,19 +84,19 @@ \section{Explore-Then-Commit}
 Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$.
 Then for the Explore-Then-Commit algorithm with parameter $m$, the expected regret after $T$ pulls with $T \ge Km$ is bounded by
 \begin{align*}
-  \mathbb{E}[R_T]
+  P[R_T]
   &\le m \sum_{a=1}^K \Delta_a + (T - Km) \sum_{a=1}^K \Delta_a \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)
   \: .
 \end{align*}
 \end{theorem}
 
 \begin{proof}\leanok
-  \uses{lem:pullCount_etcAlgorithm,def:environment,def:algorithm,lem:regret_eq_sum_pullCount_mul_gap,lem:prob_etc_error_le_exp,lem:pullCount_basic,def:pullCount}
-By Lemma~\ref{lem:regret_eq_sum_pullCount_mul_gap}, we have $\mathbb{E}[R_T] = \sum_{a=1}^K \mathbb{E}\left[N_{T,a}\right] \Delta_a$~.
-It thus suffices to bound $\mathbb{E}[N_{T,a}]$ for each arm $a$ with $\Delta_a > 0$.
+  \uses{lem:pullCount_etcAlgorithm,def:environment,def:algorithm,cor:integral_regret_eq_sum_mul,lem:prob_etc_error_le_exp,lem:pullCount_basic,def:pullCount}
+By Lemma~\ref{lem:regret_eq_sum_pullCount_mul_gap}, we have $P[R_T] = \sum_{a=1}^K P\left[N_{T,a}\right] \Delta_a$~.
+It thus suffices to bound $P[N_{T,a}]$ for each arm $a$ with $\Delta_a > 0$.
 It suffices to prove that
 \begin{align*}
-  \mathbb{E}[N_{T,a}]
+  P[N_{T,a}]
   &\le m + (T - Km) \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)
   \: .
 \end{align*}
@@ -106,6 +106,6 @@ \section{Explore-Then-Commit}
   &= m + (T - Km) \mathbb{I}\{\hat{A}_m^* = a\}
   \: .
 \end{align*}
-It thus suffices to prove the inequality $\mathbb{P}(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)$ for $\Delta_a > 0$.
+It thus suffices to prove the inequality $P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)$ for $\Delta_a > 0$.
 This is done in Lemma~\ref{lem:prob_etc_error_le_exp}.
 \end{proof}
diff --git a/blueprint/src/chapters/intro.tex b/blueprint/src/chapters/intro.tex
index e2deff4b..46a51908 100644
--- a/blueprint/src/chapters/intro.tex
+++ b/blueprint/src/chapters/intro.tex
@@ -15,3 +15,13 @@ \chapter{Introduction}
   \item the bandit model defines a probability space, on which we want to take expectations, and the theoretical study deals with random variables on that space using tools like concentration inequalities,
   \item for the experimental part, we need to be able to sample rewards from a range of probability distributions.
 \end{enumerate}
+
+\section{Notations}
+
+$P(E)$ is the probability of event $E$ under the probability distribution $P$.
+
+$P[X]$ is the expectation of random variable $X$.
+
+$P[X \mid Y]$ is the conditional expectation of random variable $X$ given random variable $Y$.
+
+$P(X \mid Y)$ is the conditional distribution of random variable $X$ given random variable $Y$.
diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex
index 4a1bf33f..653b98a9 100644
--- a/blueprint/src/chapters/ucb.tex
+++ b/blueprint/src/chapters/ucb.tex
@@ -138,7 +138,7 @@ \section{UCB}
 Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$.
 For the UCB algorithm with parameter $c \sigma^2 > 0$, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$ with positive gap, we have
 \begin{align*}
-  \mathbb{E}[N_{n,a}]
+  P[N_{n,a}]
   &\le \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2} + 2 + 2 \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}}
   \: .
 \end{align*}
@@ -157,14 +157,14 @@ \section{UCB}
 Suppose that $\nu(a)$ is $\sigma^2$-sub-Gaussian for all arms $a \in [K]$.
 For the UCB algorithm with parameter $c \sigma^2 > 0$, for any time $n \in \mathbb{N}$, we have
 \begin{align*}
-  R_n
+  P[R_n]
   &\le \sum_{a : \Delta_a > 0} \left(\frac{8 c \sigma^2 \log(n + 1)}{\Delta_a} + 2 \Delta_a\left(1 + \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}}\right)\right)
   \: .
 \end{align*}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{def:environment,def:algorithm,lem:regret_eq_sum_pullCount_mul_gap,lem:pullCount_basic,lem:expectation_pullCount_le,def:pullCount}
+  \uses{def:environment,def:algorithm,cor:integral_regret_eq_sum_mul,lem:pullCount_basic,lem:expectation_pullCount_le,def:pullCount}
 
 \end{proof}