From 9a7dccd8826d9d0b85d76c6eaf1dfb1046c42f5c Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Fri, 26 Jun 2026 14:30:11 +0200
Subject: [PATCH 1/2] bump

---
 lake-manifest.json | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index e1ac04d5..d242756a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ee89f2d4639074a91449870b8f7a0d0e401faba8",
+   "rev": "11b908e5cdd941b2d54b1b2ab55d069f5d8281d4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "ee89f2d4639074a91449870b8f7a0d0e401faba8",
+   "inputRev": "11b908e5cdd941b2d54b1b2ab55d069f5d8281d4",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8cb04559a9b9feb8efab43e135f662514561f668",
+   "rev": "c741b6f1fa5328dd0a85fab08c87de119b7fe4fe",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f",
+   "rev": "09c267c2706119a09606e6cde3f6cef5bb2ab72a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

From 0aa93bf902e1982ac82e799cf8de2cb5324d3232 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Fri, 26 Jun 2026 14:49:56 +0200
Subject: [PATCH 2/2] fix lint

---
 .../Probability/HasCondDistrib.lean           |  9 +++---
 .../Kernel/IonescuTulcea/Traj.lean            |  5 +--
 .../Online/Bandit/Algorithms/ETC.lean         | 27 ++++++----------
 .../Online/Bandit/Algorithms/UCB.lean         | 31 ++++++++-----------
 LeanMachineLearning/Online/Bandit/Regret.lean |  2 +-
 .../Algorithms/RoundRobin.lean                | 19 ++++++------
 .../BayesStationaryEnv.lean                   |  4 ---
 .../SequentialLearning/Deterministic.lean     |  6 ++--
 .../SequentialLearning/FiniteActions.lean     | 12 +++----
 lakefile.toml                                 |  2 +-
 10 files changed, 50 insertions(+), 67 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
index b60621ad..9d6da919 100644
--- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
@@ -25,7 +25,7 @@ variable {α β γ Ω Ω' : Type*}
   {μ : Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
 
 lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β} {κ : Kernel β Ω}
-    {μ : Measure α} [IsFiniteMeasure μ] {ν : Measure γ} [IsProbabilityMeasure ν]
+    {μ : Measure α} {ν : Measure γ} [IsProbabilityMeasure ν]
     (h : HasCondDistrib Y X κ μ) :
     HasCondDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) κ (μ.prod ν) where
   aemeasurable := by fun_prop
@@ -113,7 +113,7 @@ lemma HasCondDistrib.indepFun_of_const [IsProbabilityMeasure μ] {Q : Measure Ω
     h.hasLaw_of_const.map_eq, Measure.compProd_const]
 
 lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
-    (h : HasCondDistrib Y X (Kernel.const β Q) μ) [StandardBorelSpace β] [Nonempty β] :
+    (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
     HasCondDistrib X Y (Kernel.const Ω (μ.map X)) μ where
   aemeasurable := by fun_prop
   map_eq := by
@@ -124,13 +124,12 @@ lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure 
     _ = (μ.map X ⊗ₘ Kernel.const β Q).map Prod.swap := by rw [h.map_eq]
     _ = μ.map Y ⊗ₘ Kernel.const Ω (μ.map X) := by simp [h.hasLaw_of_const.map_eq, Measure.prod_swap]
 
-lemma HasLaw.prod_of_hasCondDistrib {P : Measure β} [IsFiniteMeasure μ] [IsSFiniteKernel κ]
+lemma HasLaw.prod_of_hasCondDistrib {P : Measure β}
     (h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) :
     HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ :=
   ⟨by fun_prop, by rw [h2.map_eq, h1.map_eq]⟩
 
-lemma HasCondDistrib.prod [IsFiniteMeasure μ] [IsFiniteKernel κ]
-    {Z : α → Ω'} {η : Kernel (β × Ω) Ω'} [IsFiniteKernel η]
+lemma HasCondDistrib.prod {Z : α → Ω'} {η : Kernel (β × Ω) Ω'}
     (h1 : HasCondDistrib Y X κ μ) (h2 : HasCondDistrib Z (fun ω ↦ (X ω, Y ω)) η μ) :
     HasCondDistrib (fun ω ↦ (Y ω, Z ω)) X (κ ⊗ₖ η) μ := by
   refine ⟨by fun_prop, ?_⟩
diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean
index c620a2d6..d4787afe 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean
@@ -16,7 +16,7 @@ public import Mathlib.Probability.Process.FiniteDimensionalLaws
 
 open Filter Finset Function MeasurableEquiv MeasurableSpace MeasureTheory Preorder ProbabilityTheory
 
-variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P]
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
   {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)]
   {κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)]
   {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀]
@@ -142,7 +142,8 @@ lemma eq_trajMeasure_map_frestrictLe {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw
     trajMeasure_map_frestrictLe]
 
 /-- Uniqueness of `trajMeasure`. -/
-lemma hasLaw_trajMeasure {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n))
+lemma hasLaw_trajMeasure [IsFiniteMeasure P]
+    {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n))
     (h0 : HasLaw (Y 0) μ₀ P)
     (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
     HasLaw (fun ω n ↦ Y n ω) (trajMeasure μ₀ κ) P where
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 9bdda650..c925edd5 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -63,7 +63,7 @@ variable {hK : 0 < K} {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
   {σ2 : ℝ≥0}
 
 /-- Until round `K * m - 1`, the ETC algorithm behaves like the Round-Robin algorithm. -/
-lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)]
+lemma isAlgEnvSeqUntil_roundRobinAlgorithm
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
     IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m - 1) where
   measurable_action := h.measurable_action
@@ -79,20 +79,18 @@ lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)]
 
 section AlgorithmBehavior
 
-lemma arm_zero [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
+lemma arm_zero (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
     A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ :=
   RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le)
 
-lemma arm_ae_eq_etcNextArm [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (n : ℕ) :
+lemma arm_ae_eq_etcNextArm (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (n : ℕ) :
     A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK m n (history A R n ω) := by
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   exact h.action_detAlgorithm_ae_eq n
 
 /-- For `n < K * m`, the arm pulled at time `n` is the arm `n % K`. -/
-lemma arm_of_lt [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) {n : ℕ} (hn : n < K * m) :
+lemma arm_of_lt (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
+    {n : ℕ} (hn : n < K * m) :
     A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ :=
   RoundRobin.action_ae_eq n ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono (by grind))
 
@@ -111,8 +109,7 @@ lemma arm_mul [Nonempty (Fin K)]
   exact this ▸ rfl
 
 /-- For `n ≥ K * m`, the arm pulled at time `n + 1` is the same as the arm pulled at time `n`. -/
-lemma arm_add_one_of_ge [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
+lemma arm_add_one_of_ge (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
     {n : ℕ} (hm : m ≠ 0) (hn : K * m ≤ n) :
     A (n + 1) =ᵐ[P] fun ω ↦ A n ω := by
   filter_upwards [arm_ae_eq_etcNextArm h n] with ω hn_eq
@@ -122,8 +119,7 @@ lemma arm_add_one_of_ge [Nonempty (Fin K)]
     grind
 
 /-- For `n ≥ K * m`, the arm pulled at time `n` is the same as the arm pulled at time `K * m`. -/
-lemma arm_of_ge [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
+lemma arm_of_ge (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
     {n : ℕ} (hm : m ≠ 0) (hn : K * m ≤ n) :
     A n =ᵐ[P] A (K * m) := by
   have h_ae n : K * m ≤ n → A (n + 1) =ᵐ[P] fun ω ↦ A n ω := arm_add_one_of_ge h hm
@@ -134,13 +130,11 @@ lemma arm_of_ge [Nonempty (Fin K)]
   | succ n hmn h_ind => rw [h_ae n hmn, h_ind]
 
 /-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/
-lemma pullCount_mul [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (a : Fin K) :
+lemma pullCount_mul (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (a : Fin K) :
     pullCount A a (K * m) =ᵐ[P] fun _ ↦ m :=
   RoundRobin.pullCount_mul m (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
 
-lemma pullCount_add_one_of_ge [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
+lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
     (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
     pullCount A a (n + 1)
       =ᵐ[P] fun ω ↦ pullCount A a n ω + {ω' | A (K * m) ω' = a}.indicator (fun _ ↦ 1) ω := by
@@ -150,8 +144,7 @@ lemma pullCount_add_one_of_ge [Nonempty (Fin K)]
 
 /-- For `n ≥ K * m`, the number of pulls of each arm `a` at time `n` is equal to `m` plus
 `n - K * m` if arm `a` is the best arm after the exploration phase. -/
-lemma pullCount_of_ge [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
+lemma pullCount_of_ge (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
     (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
     pullCount A a n
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator (fun _ ↦ 1) ω := by
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 2d1e2fb7..8702cb15 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -62,7 +62,7 @@ variable {hK : 0 < K} {c : ℝ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
   {σ2 : ℝ≥0} {n : ℕ} {ω : Ω}
 
 /-- Until round `K - 1`, the UCB algorithm behaves like the Round-Robin algorithm. -/
-lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)]
+lemma isAlgEnvSeqUntil_roundRobinAlgorithm
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1) where
   measurable_action := h.measurable_action
@@ -97,24 +97,21 @@ lemma ucbWidth_eq_ucbWidth' (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) (hn : n 
   norm_cast
   grind
 
-lemma arm_zero [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
+lemma arm_zero (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ :=
   RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le)
 
-lemma arm_ae_eq_ucbNextArm [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (n : ℕ) :
+lemma arm_ae_eq_ucbNextArm (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (n : ℕ) :
     A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK c n (history A R n ω) := by
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   exact h.action_detAlgorithm_ae_eq n
 
-lemma arm_ae_all_eq [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
+lemma arm_ae_all_eq (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     ∀ᵐ h ∂P, A 0 h = ⟨0, hK⟩ ∧ ∀ n, A (n + 1) h = nextArm hK c n (history A R n h) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨arm_zero h, arm_ae_eq_ucbNextArm h⟩
 
-lemma ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
+lemma ucbIndex_le_ucbIndex_arm
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) (hn : K ≤ n) :
     ∀ᵐ h ∂P, empMean A R a n h + ucbWidth A c a n h ≤
       empMean A R (A n h) n h + ucbWidth A c (A n h) n h := by
@@ -128,8 +125,7 @@ lemma ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
   exact isMaxOn_measurableArgmax (fun h a ↦ empMean' (n - 1) h a + ucbWidth' c (n - 1) h a)
     (history A R (n - 1) h) a
 
-lemma forall_arm_eq_mod_of_lt [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
+lemma forall_arm_eq_mod_of_lt (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     ∀ᵐ h ∂P, ∀ n < K, A n h = ⟨n % K, Nat.mod_lt _ hK⟩ := by
   simp_rw [ae_all_iff]
   intro n hn
@@ -141,7 +137,7 @@ lemma forall_arm_eq_mod_of_lt [Nonempty (Fin K)]
     · rfl
     · grind
 
-lemma forall_ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
+lemma forall_ucbIndex_le_ucbIndex_arm
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) :
     ∀ᵐ h ∂P, ∀ n, K ≤ n →
       empMean A R a n h + ucbWidth A c a n h ≤
@@ -149,7 +145,7 @@ lemma forall_ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
   simp_rw [ae_all_iff]
   exact fun _ ↦ ucbIndex_le_ucbIndex_arm h a
 
-lemma forall_arm_prop [Nonempty (Fin K)]
+lemma forall_arm_prop
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     ∀ᵐ h ∂P,
       (∀ n < K, A n h = ⟨n % K, Nat.mod_lt _ hK⟩) ∧
@@ -164,12 +160,12 @@ lemma forall_arm_prop [Nonempty (Fin K)]
     simp_rw [ae_all_iff] at h_ae
     exact h_ae n hn
 
-lemma time_gt_of_pullCount_gt_one [Nonempty (Fin K)]
+lemma time_gt_of_pullCount_gt_one
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n :=
   RoundRobin.time_gt_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
 
-lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)]
+lemma pullCount_pos_of_pullCount_gt_one
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω :=
   RoundRobin.pullCount_pos_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
@@ -451,7 +447,7 @@ lemma constSum_lt_top (c : ℝ) (n : ℕ) : constSum c n < ∞ := by
   positivity
 
 /-- Bound on the expectation of the number of pulls of each arm by the UCB algorithm. -/
-lemma expectation_pullCount_le' [Nonempty (Fin K)]
+lemma expectation_pullCount_le'
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) :
@@ -540,7 +536,7 @@ lemma expectation_pullCount_le' [Nonempty (Fin K)]
     positivity
 
 /-- Bound on the expectation of the number of pulls of each arm by the UCB algorithm. -/
-lemma expectation_pullCount_le [Nonempty (Fin K)]
+lemma expectation_pullCount_le
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) :
@@ -571,8 +567,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
   ring
 
 /-- Regret bound for the UCB algorithm. -/
-theorem regret_le [Nonempty (Fin K)]
-    (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
+theorem regret_le (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) :
     P[regret ν A n] ≤
diff --git a/LeanMachineLearning/Online/Bandit/Regret.lean b/LeanMachineLearning/Online/Bandit/Regret.lean
index c5b60e4f..d5e4a96d 100644
--- a/LeanMachineLearning/Online/Bandit/Regret.lean
+++ b/LeanMachineLearning/Online/Bandit/Regret.lean
@@ -90,7 +90,7 @@ lemma integral_regret_eq_sum_gap_mul_integral_pullCount
 /-- 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]
+    [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) :
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean
index 2476ad31..14c8cf35 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean
@@ -91,19 +91,19 @@ variable {hK : 0 < K} {ν : Kernel (Fin K) 𝓨} [IsMarkovKernel ν]
   {P : Measure Ω} [IsProbabilityMeasure P]
   {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨}
 
-lemma action_zero [Nonempty (Fin K)]
+lemma action_zero
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P 0) :
     A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := by
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   exact h.action_zero_detAlgorithm
 
-lemma action_ae_eq_roundRobinNextAction [Nonempty (Fin K)] (n : ℕ)
+lemma action_ae_eq_roundRobinNextAction (n : ℕ)
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (n + 1)) :
     A (n + 1) =ᵐ[P] fun _ ↦ nextAction hK n :=
   h.action_detAlgorithm_ae_eq (by grind)
 
 /-- The action chosen at time `n` is the action `n % K`. -/
-lemma action_ae_eq [Nonempty (Fin K)] (n : ℕ)
+lemma action_ae_eq (n : ℕ)
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P n) :
     A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := by
   cases n with
@@ -113,7 +113,7 @@ lemma action_ae_eq [Nonempty (Fin K)] (n : ℕ)
     rw [hn_eq, nextAction]
 
 /-- At time `K * m`, the number of times each action is chosen is equal to `m`. -/
-lemma pullCount_mul [Nonempty (Fin K)] (m : ℕ)
+lemma pullCount_mul (m : ℕ)
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m - 1))
     (a : Fin K) :
     pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := by
@@ -129,15 +129,14 @@ lemma pullCount_mul [Nonempty (Fin K)] (m : ℕ)
     sum_congr rfl fun s hs ↦ by rw [h_arm' hs]
   _ = m := sum_mod_range_mul hK m a
 
-lemma pullCount_eq_one [Nonempty (Fin K)]
-    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1))
-    (a : Fin K) :
+lemma pullCount_eq_one
+    (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) :
     pullCount A a K =ᵐ[P] fun _ ↦ 1 := by
   suffices pullCount A a (K * 1) =ᵐ[P] fun _ ↦ 1 by simpa using this
   refine pullCount_mul 1 (P := P) (ν := ν) (Y := Y) (hK := hK) ?_ a
   simpa
 
-lemma time_gt_of_pullCount_gt_one [Nonempty (Fin K)]
+lemma time_gt_of_pullCount_gt_one
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n := by
   filter_upwards [pullCount_eq_one h a] with h h_eq n hn
@@ -145,7 +144,7 @@ lemma time_gt_of_pullCount_gt_one [Nonempty (Fin K)]
   by_contra! h_lt
   exact hn.not_ge (pullCount_mono _ h_lt _)
 
-lemma pullCount_pos_of_time_ge [Nonempty (Fin K)]
+lemma pullCount_pos_of_time_ge
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) :
     ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω := by
   have h_ae a := pullCount_eq_one h a
@@ -155,7 +154,7 @@ lemma pullCount_pos_of_time_ge [Nonempty (Fin K)]
   rw [← hω a]
   exact pullCount_mono _ hn _
 
-lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)]
+lemma pullCount_pos_of_pullCount_gt_one
     (h : IsAlgEnvSeqUntil A Y (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω := by
   filter_upwards [time_gt_of_pullCount_gt_one h a, pullCount_pos_of_time_ge h] with ω h1 h2 n h_gt a
diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
index 3a93e553..68cc8ffe 100644
--- a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
@@ -166,7 +166,6 @@ def bayesStationaryEnv (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel
     (Kernel.deterministic (Prod.fst ∘ g) (by fun_prop)) ×ₖ (κ.comap g (by fun_prop))
   ν0 := (Kernel.const _ Q) ⊗ₖ κ.swapLeft
 
-variable [Nonempty 𝓐] [StandardBorelSpace 𝓐]
 variable {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × 𝓐) 𝓨} [IsMarkovKernel κ]
 variable {alg : Algorithm 𝓐 𝓨} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓔 × 𝓨}
 variable {P : Measure Ω} [IsProbabilityMeasure P]
@@ -216,9 +215,6 @@ def bayesTrajMeasure (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (
 deriving IsProbabilityMeasure
 
 lemma isBayesAlgEnvSeq_bayesTrajMeasure
-    [StandardBorelSpace 𝓐] [Nonempty 𝓐]
-    [StandardBorelSpace 𝓔] [Nonempty 𝓔]
-    [StandardBorelSpace 𝓨] [Nonempty 𝓨]
     (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) [IsMarkovKernel κ]
     (alg : Algorithm 𝓐 𝓨) :
     IsBayesAlgEnvSeq Q κ alg (fun ω ↦ (ω 0).2.1) action (fun n ω ↦ (ω n).2.2)
diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
index abbcfffa..d9a40ac7 100644
--- a/LeanMachineLearning/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -262,12 +262,12 @@ lemma action_zero_detAlgorithm [MeasurableEq 𝓐]
     A 0 =ᵐ[P] fun _ ↦ action0 :=
   (IsDeterministicAlg.action_zero_ae_eq h).trans (by simp)
 
-lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐] [Nonempty 𝓐]
+lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐]
     (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) (n : ℕ) :
     A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) :=
   (IsDeterministicAlg.action_ae_eq h n).trans (by simp)
 
-lemma action_detAlgorithm_ae_all_eq [MeasurableEq 𝓐] [Nonempty 𝓐]
+lemma action_detAlgorithm_ae_all_eq [MeasurableEq 𝓐]
     (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) :
     ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextA n (history A Y n ω) := by
   filter_upwards [IsDeterministicAlg.action_ae_all_eq h] with ω hω using by simp [hω]
@@ -290,7 +290,7 @@ lemma action_zero_detAlgorithm [MeasurableEq 𝓐]
     A 0 =ᵐ[P] fun _ ↦ action0 :=
   (IsDeterministicAlg.action_zero_of_IsAlgEnvSeqUntil h).trans (by simp)
 
-lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐] [Nonempty 𝓐]
+lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐]
     (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) (hn : n < N) :
     A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) :=
   (IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp)
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index 8a13a8e7..806bc7cb 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -939,7 +939,7 @@ lemma measurable_uncurry_empMean' [MeasurableEq 𝓐] (n : ℕ) :
   unfold empMean'
   fun_prop
 
-lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
     IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
@@ -960,7 +960,7 @@ lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] [Nonempty 
     exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback).mono
       (by lia)) le_rfl
 
-lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one [StandardBorelSpace 𝓐]
     {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
     StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
@@ -969,7 +969,7 @@ lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one [StandardBorelSpace 𝓐] [
   rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
-lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
     Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
@@ -999,7 +999,7 @@ lemma _root_.MeasureTheory.StronglyMeasurable.div₀' {𝓐 β : Type*}
 
 end CopiedFromPR
 
-lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
     IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
@@ -1010,7 +1010,7 @@ lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] [Nonempty 𝓐
   · have h_meas := (isPredictable_pullCount h.measurable_action h.measurable_feedback a).measurable
     fun_prop
 
-lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one [StandardBorelSpace 𝓐]
     {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
     StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
@@ -1019,7 +1019,7 @@ lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one [StandardBorelSpace 𝓐] [Non
   rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
-lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] [Nonempty 𝓐] {R' : ℕ → Ω → ℝ}
+lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
     {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
     (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
     Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
diff --git a/lakefile.toml b/lakefile.toml
index 35dd9f5a..5a9ba3fb 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -17,7 +17,7 @@ rev = "main"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "ee89f2d4639074a91449870b8f7a0d0e401faba8"
+rev = "11b908e5cdd941b2d54b1b2ab55d069f5d8281d4"
 
 [[lean_lib]]
 name = "LeanMachineLearning"