Update Mathlib and fix lint errors

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, ?_⟩

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

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

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,15 +137,15 @@ 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 ≤
         empMean A R (A n h) n h + ucbWidth A c (A n h) n h := by
   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] ≤

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) :

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,23 +129,22 @@ 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
   rw [← h_eq] at hn
   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

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)

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)