From 357e9dd450b76d6ff85955280bb4721a2c520442 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Thu, 10 Sep 2026 16:39:39 +0200
Subject: [PATCH] Update Mathlib

---
 .../KullbackLeibler/MapSequence.lean          |  2 +-
 .../MeasurableSpace/Embedding.lean            |  4 +-
 .../Probability/HasCondDistrib.lean           | 11 +--
 .../Probability/Independence/CondDistrib.lean | 57 +++++++-------
 .../Probability/Independence/IndepFun.lean    |  1 -
 .../ForMathlib/Probability/WithDensity.lean   | 75 +------------------
 .../Online/Bandit/Algorithms/ETC.lean         |  2 +-
 .../Algorithms/Regret/BayesRegretTS.lean      |  3 +-
 .../Online/Bandit/Algorithms/TS.lean          |  3 +-
 .../Online/Bandit/ArrayProbSpace.lean         |  2 +-
 .../Online/Bandit/RewardByCountMeasure.lean   |  9 +--
 .../Online/Bandit/SumRewards.lean             |  4 +-
 .../SequentialLearning/AlgorithmDensity.lean  |  6 +-
 .../AlgorithmDensityBayes.lean                | 10 ++-
 .../Algorithms/RandomSampling/Tendsto.lean    |  2 -
 .../BayesStationaryEnv.lean                   |  2 +-
 .../DivergenceDecomposition.lean              |  4 +-
 lake-manifest.json                            |  8 +-
 lakefile.toml                                 |  2 +-
 19 files changed, 65 insertions(+), 142 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean
index 7b1f1adc..a2797244 100644
--- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean
+++ b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean
@@ -184,7 +184,7 @@ lemma iSup_comap_restrictFin {E : Type*} [mE : MeasurableSpace E] :
     ⨆ n : ℕ, MeasurableSpace.comap (fun f : ℕ → E ↦ fun i : Fin n ↦ f i)
       MeasurableSpace.pi = MeasurableSpace.pi := by
   refine le_antisymm
-    (iSup_le fun n ↦ (measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _).comap_le)
+    (iSup_le fun n ↦ (Measurable.of_eval fun _ ↦ measurable_pi_apply _).comap_le)
     (iSup_le fun i ↦ le_iSup_of_le (i + 1) ?_)
   have : (fun f : ℕ → E ↦ f i) =
       (fun h : Fin (i + 1) → E ↦ h ⟨i, i.lt_succ_self⟩) ∘
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean
index 859212b0..4fca8151 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean
@@ -129,8 +129,8 @@ def finSuccPiIic (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] (n : ℕ) :
   invFun h i := h ⟨i.1, mem_Iic.mpr (Nat.le_of_lt_succ i.2)⟩
   left_inv _ := rfl
   right_inv _ := rfl
-  measurable_toFun := measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _
-  measurable_invFun := measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _
+  measurable_toFun := .of_eval fun _ ↦ measurable_pi_apply _
+  measurable_invFun := .of_eval fun _ ↦ measurable_pi_apply _
 
 @[simp]
 lemma finSuccPiIic_apply (n : ℕ) (h : Π i : Fin (n + 1), X i) (i : Iic n) :
diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
index 03af128e..93e9c492 100644
--- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
@@ -272,7 +272,8 @@ lemma _root_.MeasureTheory.Measure.dirac_compProd {κ : Kernel β Ω} [IsSFinite
 lemma hasCondDistrib_const_iff [IsProbabilityMeasure μ] [IsSFiniteKernel κ] {b : β} :
     HasCondDistrib Y (fun _ ↦ b) κ μ ↔ HasLaw Y (κ b) μ := by
   refine ⟨fun h ↦ ⟨h.aemeasurable_snd, ?_⟩, fun h ↦ ⟨aemeasurable_const.prodMk h.aemeasurable, ?_⟩⟩
-  · rw [← Measure.snd_map_prodMk₀ (X := fun _ ↦ b) (Y := Y) aemeasurable_const, h.map_eq,
+  · rw [← Measure.snd_map_prodMk₀ (X := fun _ ↦ b) (Y := Y) aemeasurable_const
+      h.aemeasurable_snd, h.map_eq,
       Measure.map_const, measure_univ, one_smul, Measure.dirac_compProd, Measure.snd,
       Measure.map_map measurable_snd measurable_prodMk_left]
     exact Measure.map_id
@@ -346,14 +347,14 @@ variable [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω'] [Nonempt
 lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
     (h : HasCondDistrib Y X κ μ) :
     condDistrib Y X μ =ᵐ[μ.map X] κ := by
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h.map_eq]
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd h.aemeasurable_fst h.aemeasurable_snd, h.map_eq]
 
 lemma hasCondDistrib_of_condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
     (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
     (h : condDistrib Y X μ =ᵐ[μ.map X] κ) :
     HasCondDistrib Y X κ μ where
   aemeasurable := by fun_prop
-  map_eq := by rw [← compProd_map_condDistrib hY, Measure.compProd_congr h]
+  map_eq := by rw [← compProd_map_condDistrib hX hY, Measure.compProd_congr h]
 
 lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]
     {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω}
@@ -367,8 +368,8 @@ lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpa
     exact hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) hz
   have h_eq : condDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) μ
       =ᵐ[μ.map Z ⊗ₘ (condDistrib W Z μ).map f] η := by
-    rw [← Measure.compProd_congr (condDistrib_comp Z hW hf),
-        compProd_map_condDistrib (hf.comp_aemeasurable hW)]
+    rw [← Measure.compProd_congr (condDistrib_comp hcd.aemeasurable_fst.fst hW hf),
+        compProd_map_condDistrib hcd.aemeasurable_fst.fst (hf.comp_aemeasurable hW)]
     exact hcd.condDistrib_eq
   filter_upwards [
     condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_fst.fst,
diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
index 5b3c7a2b..b4de6ce5 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
@@ -33,22 +33,19 @@ section CondDistrib
 
 variable [IsFiniteMeasure μ]
 
-lemma map_swap_compProd_map_condDistrib (hY : AEMeasurable Y μ) :
+lemma map_swap_compProd_map_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
     (μ.map X ⊗ₘ condDistrib Y X μ).map Prod.swap = μ.map (fun a ↦ (Y a, X a)) := by
-  by_cases hX : AEMeasurable X μ
-  · rw [compProd_map_condDistrib hY,
-      AEMeasurable.map_map_of_aemeasurable measurable_swap.aemeasurable (hX.prodMk hY)]
-    rfl
-  · have hYX : ¬ AEMeasurable (fun a ↦ (Y a, X a)) μ :=
-      fun h ↦ hX (measurable_snd.comp_aemeasurable h)
-    simp [hX, hYX]
+  rw [compProd_map_condDistrib hX hY,
+    AEMeasurable.map_map_of_aemeasurable measurable_swap.aemeasurable (hX.prodMk hY)]
+  rfl
 
 lemma condDistrib_prod_left [StandardBorelSpace β] [Nonempty β]
     (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :
     condDistrib (fun ω ↦ (X ω, Y ω)) T μ
       =ᵐ[μ.map T] condDistrib X T μ ⊗ₖ condDistrib Y (fun ω ↦ (T ω, X ω)) μ := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) T (by fun_prop) ?_
-  rw [← Measure.compProd_assoc', compProd_map_condDistrib hX, compProd_map_condDistrib hY,
+  refine condDistrib_ae_eq_of_measure_eq_compProd hT (by fun_prop) ?_
+  rw [← Measure.compProd_assoc', compProd_map_condDistrib hT hX,
+    compProd_map_condDistrib (hT.prodMk hX) hY,
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
   rfl
 
@@ -60,8 +57,8 @@ lemma condDistrib_condDistrib_ae_eq_sectR_condDistrib [StandardBorelSpace β] [N
         (condDistrib (g ∘ Z) (fun a ↦ (T a, (f ∘ Z) a)) μ).sectR t := by
   filter_upwards [
     condDistrib_prod_left (hf.comp_aemeasurable hZ) (hg.comp_aemeasurable hZ) hT,
-    condDistrib_comp T hZ (hf.prodMk hg), condDistrib_comp T hZ hf] with t h_prod h_pair h_fst
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd f hg.aemeasurable]
+    condDistrib_comp hT hZ (hf.prodMk hg), condDistrib_comp hT hZ hf] with t h_prod h_pair h_fst
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd hf.aemeasurable hg.aemeasurable]
   calc (condDistrib Z T μ t).map (fun ω' ↦ (f ω', g ω'))
   _ = condDistrib (fun a ↦ ((f ∘ Z) a, (g ∘ Z) a)) T μ t := by
       rw [← Kernel.map_apply _ (hf.prodMk hg)]
@@ -75,8 +72,9 @@ lemma condDistrib_prod_self_left [StandardBorelSpace β] [Nonempty β] [Standard
     (hX : AEMeasurable X μ) (hT : AEMeasurable T μ) :
     condDistrib (fun ω ↦ (X ω, T ω)) T μ =ᵐ[μ.map T] condDistrib X T μ ×ₖ Kernel.id := by
   have h_prod := condDistrib_prod_left hX hT hT (μ := μ)
-  have h_fst := condDistrib_comp_self (μ := μ) (fun ω ↦ (T ω, X ω)) (f := Prod.fst) (by fun_prop)
-  rw [(compProd_map_condDistrib hX).symm] at h_fst
+  have h_fst := condDistrib_comp_self (μ := μ) (X := fun ω ↦ (T ω, X ω)) (f := Prod.fst)
+    (hT.prodMk hX) measurable_fst
+  rw [(compProd_map_condDistrib hT hX).symm] at h_fst
   have h_fst' := (Measure.ae_compProd_iff (Kernel.measurableSet_eq _ _)).mp h_fst
   filter_upwards [h_prod, h_fst'] with z hz1 hz2
   rw [hz1]
@@ -104,9 +102,9 @@ lemma CondIndepFun.prod_right [StandardBorelSpace α] [StandardBorelSpace β] [N
     (h : X ⟂ᵢ[Z, hZ; μ] Y) :
     X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, Z ω)) := by
   rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ,
-    condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h
+    condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h
   rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) hX hZ,
-    condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]
+    condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)]
   -- Key: condDistrib (Y, Z) Z μ z = (condDistrib Y Z μ z).map (y ↦ (y, z))
   have h_cond : condDistrib (fun ω ↦ (Y ω, Z ω)) Z μ =ᵐ[μ.map Z]
       fun z ↦ (condDistrib Y Z μ z).map (fun y ↦ (y, z)) := by
@@ -149,14 +147,14 @@ lemma fst_condDistrib_prod [StandardBorelSpace β] [Nonempty β]
 
 lemma condDistrib_of_indepFun (h : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
     condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) X hY ?_
+  refine condDistrib_ae_eq_of_measure_eq_compProd hX hY ?_
   simp only [Measure.compProd_const]
   exact (indepFun_iff_map_prod_eq_prod_map_map hX hY).mp h
 
 lemma indepFun_iff_condDistrib_eq_const (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
     IndepFun X Y μ ↔ condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by
   refine ⟨fun h ↦ condDistrib_of_indepFun h hX hY, fun h ↦ ?_⟩
-  rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hY,
+  rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hX hY,
     Measure.compProd_congr h]
   simp
 
@@ -275,9 +273,9 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight
     (h : condDistrib Y (fun ω ↦ (Z ω, X ω)) μ =ᵐ[μ.map (fun ω ↦ (Z ω, X ω))] η.prodMkRight _) :
     Y ⟂ᵢ[Z, hZ; μ] X := by
   have hη_eq : condDistrib Y Z μ =ᵐ[μ.map Z] η := by
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h ⊢
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h ⊢
     have h_fst : μ.map Z = (μ.map (fun ω ↦ (Z ω, X ω))).fst := by
-      rw [Measure.fst_map_prodMk hX]
+      rw [Measure.fst_map_prodMk hZ hX]
     rw [h_fst, ← Measure.map_swap_comprod_eq_fst_compProd, ← h,
       Measure.map_map (by fun_prop) (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop),
       Measure.fst,
@@ -286,7 +284,7 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight
   symm
   rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ]
   refine h.trans ?_
-  rw [Kernel.prodMkRight_ae_eq_iff, Measure.fst_map_prodMk (by fun_prop)]
+  rw [Kernel.prodMkRight_ae_eq_iff, Measure.fst_map_prodMk (by fun_prop) (by fun_prop)]
   exact hη_eq.symm
 
 omit [StandardBorelSpace Ω'] [Nonempty Ω'] in
@@ -297,7 +295,7 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
     (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) :
     Y ⟂ᵢ[Z, hZ; μ] X := by
   refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight hX hY hZ ?_ (η := η)
-  rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop)] at h ⊢
+  rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop) (by fun_prop)] at h ⊢
   have : μ.map (fun a ↦ ((Z a, X a), Y a))
       = (μ.map (fun a ↦ ((X a, Z a), Y a))).map (fun p ↦ ((p.1.2, p.1.1), p.2)) := by
     rw [Measure.map_map (by fun_prop) (by fun_prop)]
@@ -333,9 +331,9 @@ lemma condIndepFun_fst_prod [StandardBorelSpace α] [StandardBorelSpace β] [Non
   rw [condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib (by fun_prop)
     (by fun_prop) (by fun_prop)] at h_indep ⊢
   have h1 : 𝓛[fun ω ↦ Y ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[Y | Z; μ] :=
-    condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop)
+    condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop) (by fun_prop)
   have h2 : 𝓛[fun ω ↦ X ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[X | Z; μ] :=
-    condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop)
+    condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop) (by fun_prop)
   have h_fst1 : (μ.prod ν).map (fun ω ↦ Z ω.1) = μ.map Z := by
     conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,
       Measure.map_map (by fun_prop) (by fun_prop)]
@@ -417,8 +415,8 @@ lemma ae_eq_of_map_prodMk_eq {β Ω : Type*} {_ : MeasurableSpace β} {_ : Measu
 lemma ae_eq_of_condDistrib_eq_deterministic {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ)
     (hY : AEMeasurable Y μ) (h : condDistrib Y X μ =ᵐ[μ.map X] Kernel.deterministic f hf) :
     Y =ᵐ[μ] f ∘ X := by
-  have hfX := condDistrib_comp_self (μ := μ) X hf
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h hfX
+  have hfX := condDistrib_comp_self hX hf
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd hX (by fun_prop)] at h hfX
   exact ae_eq_of_map_prodMk_eq hf hX hY (hfX ▸ h)
 
 end CondDistrib
@@ -432,7 +430,7 @@ lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β]
   rw [Filter.EventuallyEq, ae_iff_of_countable]
   intro b hb
   ext s hs
-  rw [condDistrib_apply_of_ne_zero hY,
+  rw [condDistrib_apply_of_ne_zero hX hY,
     Measure.map_apply hX (measurableSet_singleton _), Measure.map_apply hY hs,
     Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs),
     cond_apply (hX (measurableSet_singleton _))]
@@ -451,7 +449,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     (h_cond : ∀ b, μ (Z ⁻¹' {b}) ≠ 0 → condDistrib Y X μ[|Z ⁻¹' {b}] =ᵐ[μ[|Z ⁻¹' {b}].map X]
       (κ.comap (fun ω ↦ (ω, b)) (by fun_prop) : Kernel β Ω)) :
     condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] κ := by
-  refine condDistrib_ae_eq_of_measure_eq_compProd _ (by fun_prop) ?_
+  refine condDistrib_ae_eq_of_measure_eq_compProd (by fun_prop) (by fun_prop) ?_
   ext s hs
   suffices ∀ b, (Measure.map (fun x ↦ ((X x, Z x), Y x)) μ) (s ∩ {p | p.1.2 = b}) =
       (Measure.map (fun ω ↦ (X ω, Z ω)) μ ⊗ₘ κ) (s ∩ {p | p.1.2 = b}) by
@@ -503,8 +501,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
       exact .inr hb
     rw [h_left, h_right]
   specialize h_cond b hb
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd] at h_cond
-  swap; · fun_prop
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h_cond
   rw [Measure.ext_iff] at h_cond
   have hs' : MeasurableSet {p : β × Ω | ((p.1, b), p.2) ∈ s} := hs.preimage (by fun_prop)
   have h1 := h_cond {p | ((p.1, b), p.2) ∈ s} hs'
diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean
index 93dbf147..297c9c4b 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean
@@ -130,7 +130,6 @@ lemma IndepFun_map_iff [IsFiniteMeasure μ] {X : Ω' → E} {Y : Ω' → E} {f :
 lemma iIndepFun_map_iff [IsProbabilityMeasure μ] {X : ι → Ω' → E} {f : Ω → Ω'}
     (hf : AEMeasurable f μ) (hX : ∀ n, AEMeasurable (X n) (μ.map f)) :
     iIndepFun X (μ.map f) ↔ iIndepFun (fun n ↦ X n ∘ f) μ := by
-  have := Measure.isProbabilityMeasure_map hf (μ := μ)
   rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀' hX,
     iIndepFun_iff_map_fun_eq_infinitePi_map₀' (by fun_prop)]
   rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
diff --git a/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean b/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean
index eef5d6b7..98050883 100644
--- a/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Probability.Kernel.CompProdEqIff
 public import Mathlib.Probability.Kernel.Composition.MeasureComp
+public import Mathlib.Probability.Kernel.Composition.WithDensity
 
 /-! # Lemmas about kernels and measures with density
 -/
@@ -45,29 +46,6 @@ end MeasureTheory
 
 namespace MeasureTheory.Measure
 
-lemma compProd_withDensity_left [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] {f : α → ℝ≥0∞}
-    (hf : Measurable f) : (μ.withDensity f) ⊗ₘ κ = (μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1) := by
-  refine ext_of_lintegral _ fun g hg ↦ ?_
-  calc ∫⁻ ab, g ab ∂((μ.withDensity f) ⊗ₘ κ)
-      = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂(μ.withDensity f) :=
-        lintegral_compProd hg
-    _ = ∫⁻ a, f a * ∫⁻ b, g (a, b) ∂κ a ∂μ :=
-        lintegral_withDensity_eq_lintegral_mul _ hf hg.lintegral_kernel_prod_right'
-    _ = ∫⁻ a, ∫⁻ b, f a * g (a, b) ∂κ a ∂μ :=
-        lintegral_congr fun a ↦ (lintegral_const_mul _ (by fun_prop)).symm
-    _ = ∫⁻ ab, (fun ab ↦ f ab.1) ab * g ab ∂(μ ⊗ₘ κ) :=
-        (lintegral_compProd ((hf.comp measurable_fst).mul hg)).symm
-    _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)) :=
-        (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_fst) hg).symm
-
-lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ]
-    {f : α → ℝ≥0∞} {g : α → β → ℝ≥0∞} (hf : Measurable f) (hg : Measurable (Function.uncurry g))
-    [IsSFiniteKernel (κ.withDensity g)] :
-    (μ.withDensity f) ⊗ₘ (κ.withDensity g) =
-      (μ ⊗ₘ κ).withDensity (fun ac ↦ f ac.1 * g ac.1 ac.2) := by
-  rw [compProd_withDensity hg, compProd_withDensity_left hf]
-  exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm
-
 lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α β} [IsSFiniteKernel κ]
     [IsSFiniteKernel η] {f : β → ℝ≥0∞} (hf : Measurable f)
     (h : κ =ᵐ[μ] η.withDensity (fun _ b ↦ f b)) :
@@ -93,57 +71,6 @@ end MeasureTheory.Measure
 
 namespace ProbabilityTheory.Kernel
 
-lemma comp_withDensity_eq_withDensity_comp {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞}
-    (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f := by
-  refine Measure.ext_of_lintegral _ fun g hg ↦ ?_
-  calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ)
-      = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ :=
-        Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable
-    _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by
-        congr with a
-        exact lintegral_withDensity _ (by fun_prop) _ hg
-    _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) :=
-        (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm
-    _ = ∫⁻ b, g b ∂((κ ∘ₘ μ).withDensity f) :=
-        (lintegral_withDensity_eq_lintegral_mul _ hf hg).symm
-
-lemma compProd_withDensity_left {κ : Kernel α β} {η : Kernel (α × β) γ} {f : α → β → ℝ≥0∞}
-    [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (κ.withDensity f)]
-    (hf : Measurable (Function.uncurry f)) :
-    (κ.withDensity f) ⊗ₖ η = (κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1) := by
-  ext a : 1
-  calc ((κ.withDensity f) ⊗ₖ η) a
-      = (κ a).withDensity (f a) ⊗ₘ η.sectR a := by
-        rw [compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ hf]
-    _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun bc ↦ f a bc.1) :=
-        Measure.compProd_withDensity_left (by fun_prop)
-    _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)) a := by
-        rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)]
-
-lemma sectR_withDensity {η : Kernel (α × β) γ} {g : α × β → γ → ℝ≥0∞} [IsSFiniteKernel η]
-    (hg : Measurable (Function.uncurry g)) (a : α) :
-    (η.withDensity g).sectR a = (η.sectR a).withDensity (fun b ↦ g (a, b)) := by
-  ext b s hs
-  rw [Kernel.sectR_apply, Kernel.withDensity_apply' _ hg,
-    Kernel.withDensity_apply' _ (by fun_prop), Kernel.sectR_apply]
-
-lemma compProd_withDensity_right {κ : Kernel α β} {η : Kernel (α × β) γ} {g : α × β → γ → ℝ≥0∞}
-    [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (η.withDensity g)]
-    (hg : Measurable (Function.uncurry g)) :
-    κ ⊗ₖ (η.withDensity g) = (κ ⊗ₖ η).withDensity (fun a bc ↦ g (a, bc.1) bc.2) := by
-  ext a : 1
-  have h_sf : IsSFiniteKernel ((η.sectR a).withDensity (fun b ↦ g (a, b))) := by
-    rw [← sectR_withDensity hg]
-    infer_instance
-  calc (κ ⊗ₖ (η.withDensity g)) a
-      = (κ a) ⊗ₘ ((η.withDensity g).sectR a) := compProd_apply_eq_compProd_sectR ..
-    _ = (κ a) ⊗ₘ ((η.sectR a).withDensity (fun b ↦ g (a, b))) := by rw [sectR_withDensity hg]
-    _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun p ↦ g (a, p.1) p.2) := by
-        refine Measure.compProd_withDensity ?_
-        fun_prop
-    _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ g (a, bc.1) bc.2)) a := by
-        rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)]
-
 lemma withDensity_rnDeriv_eq' {κ η : Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β]
     [IsFiniteKernel κ] [IsFiniteKernel η] (h : ∀ a, κ a ≪ η a) :
     η.withDensity (κ.rnDeriv η) = κ :=
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index f6a53d31..9cc758ed 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -185,7 +185,7 @@ lemma probReal_sumRewards_le_sumRewards_le [Nonempty (Fin K)]
   simp_rw [measureReal_def]
   congr 1
   refine measure_congr ?_
-  rw [Filter.eventuallyEq_set]
+  rw [Filter.eventuallyEqSet_iff]
   filter_upwards [pullCount_mul h a, pullCount_mul h (bestArm ν)] with ω ha h_best
   simp [ha, h_best]
 
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
index a9e39543..61ed53ac 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
@@ -328,7 +328,8 @@ lemma integral_ucb_action_eq_integral_ucb_bestAction (hK : 0 < K)
     _ = ∫ ha, uc ha ∂P.map (fun ω ↦ (history (noObs Ω) A R n ω, A n ω)) := by
         rw [← integral_map (by fun_prop) (by fun_prop)]
     _ = ∫ ha, uc ha ∂P.map (fun ω ↦ (history (noObs Ω) A R n ω, bestAction κ E ω)) := by
-        rw [← compProd_map_condDistrib (by fun_prop), ← compProd_map_condDistrib (by fun_prop),
+        rw [← compProd_map_condDistrib (by fun_prop) (by fun_prop),
+          ← compProd_map_condDistrib (by fun_prop) (by fun_prop),
             Measure.compProd_congr (hasCondDistrib_action hK h n).condDistrib_eq]
     _ = P[fun ω ↦ ucb A R l u σ2 δ (bestAction κ E ω) n ω] := by
         rw [integral_map (by fun_prop) (by fun_prop)]
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean
index e4982c72..22e8a86c 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean
@@ -117,6 +117,7 @@ lemma TS.hasCondDistrib_action (hK : 0 < K) (h : IsBayesAlgEnvSeq Q κ (tsAlgori
           simp_rw [Kernel.map_apply _ hm, IT.bayesTrajMeasurePosterior, hc]
       _ =ᵐ[P.map (history (noObs Ω) A R n)]
           condDistrib (bestAction κ E) (history (noObs Ω) A R n) P :=
-          (condDistrib_comp (history (noObs Ω) A R n) h.measurable_param.aemeasurable hm).symm
+          (condDistrib_comp (measurable_history (fun _ ↦ measurable_const) h.measurable_action
+            h.measurable_feedback n).aemeasurable h.measurable_param.aemeasurable hm).symm
 
 end Bandits
diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
index d650f43a..3bbfc3a6 100644
--- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
+++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
@@ -208,7 +208,7 @@ def truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) (ω : probSpace 𝓐 𝓡)
 lemma measurable_truncRow [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) :
     Measurable (truncRow a m : probSpace 𝓐 𝓡 → probSpace 𝓐 𝓡) := by
   refine Measurable.prodMk measurable_fst
-    (measurable_pi_lambda _ fun i ↦ measurable_pi_lambda _ fun b ↦ ?_)
+    (.of_eval fun i ↦ .of_eval fun b ↦ ?_)
   by_cases hb : b = a <;> simp only [hb, ↓reduceIte] <;> fun_prop
 
 variable [Nonempty 𝓐] [StandardBorelSpace 𝓐]
diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
index 902d6c53..fe804ee9 100644
--- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
@@ -46,7 +46,7 @@ lemma condDistrib_reward'' [Countable 𝓐]
   rw [h_law]
   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) _
+    condDistrib_fst_prod (by fun_prop) (by fun_prop) _
   filter_upwards [h_ra', h_prod] with ω h_eq h_prod
   rw [h_prod, h_eq]
 
@@ -195,10 +195,7 @@ lemma hasLaw_rewardByCount [StandardBorelSpace Ω] [Countable 𝓐]
       rw [condDistrib_comp_map (by fun_prop) (by fun_prop)]
     _ = (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)) :=
-        Measure.isProbabilityMeasure_map (by fun_prop)
-      simp
+    _ = ν a := by simp
 
 lemma identDistrib_rewardByCount [StandardBorelSpace Ω] [Countable 𝓐]
     (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (n m : ℕ)
@@ -439,7 +436,7 @@ lemma hasLaw_rewardByCount_infinitePi (h : IsAlgEnvSeq O A R alg (stationaryEnv
     HasLaw (fun ω (p : 𝓐 × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1) ω)
       (Measure.infinitePi fun p : 𝓐 × ℕ ↦ ν p.1) 𝔓 := by
   have hY : Measurable fun ω (p : 𝓐 × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1) ω :=
-    measurable_pi_lambda _ fun p ↦
+    .of_eval fun p ↦
       measurable_rewardByCount h.measurable_action h.measurable_feedback p.1 (p.2 + 1)
   -- `rewardByCountUntil A R t` has that law for all `t` and converges entrywise to the array
   exact hasLaw_of_forall_eventually_eq (L := Filter.atTop)
diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean
index 1719cfd0..b10ef735 100644
--- a/LeanMachineLearning/Online/Bandit/SumRewards.lean
+++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean
@@ -715,7 +715,7 @@ lemma prob_empMean_sub_actionMean_ge_le (h : IsBayesAlgEnvSeq Q κ alg E A R P)
         rw [empMean] at hle
         exact ⟨a, t, ht, hpc, sqrt_two_mul_le_sub hpc hle⟩
     _ = (P.map E ⊗ₘ condDistrib (trajectory (noObs Ω) A R) E P) S := by
-        rw [← compProd_map_condDistrib (by fun_prop)]
+        rw [← compProd_map_condDistrib (by fun_prop) (by fun_prop)]
     _ = ∫⁻ e, condDistrib (trajectory (noObs Ω) A R) E P e (Prod.mk e ⁻¹' S) ∂(P.map E) :=
         Measure.compProd_apply (by measurability)
     _ ≤ ∫⁻ e, ENNReal.ofReal (Fintype.card (Fin K) * (n - 1) * δ) ∂(P.map E) := by
@@ -756,7 +756,7 @@ lemma prob_empMean_bestAction_sub_actionMean_le_le (h : IsBayesAlgEnvSeq Q κ al
         rw [empMean] at hle
         exact ⟨t, ht, hpc, sub_le_neg_sqrt_two_mul hpc hle⟩
     _ = (P.map E ⊗ₘ condDistrib (trajectory (noObs Ω) A R) E P) S := by
-        rw [← compProd_map_condDistrib (by fun_prop)]
+        rw [← compProd_map_condDistrib (by fun_prop) (by fun_prop)]
     _ = ∫⁻ e, condDistrib (trajectory (noObs Ω) A R) E P e (Prod.mk e ⁻¹' S) ∂(P.map E) :=
         Measure.compProd_apply (by measurability)
     _ ≤ ∫⁻ e, ENNReal.ofReal ((n - 1) * δ) ∂(P.map E) := by
diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
index 4ea64b4e..53dd65a8 100644
--- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
+++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
@@ -144,12 +144,12 @@ lemma hasLaw_history_withDensity (h : IsAlgEnvSeq O A Y alg env P)
             = (alg₀.policy n ⊗ₖ env.feedback n).withDensity
               (fun p ar ↦ Kernel.rnDeriv (alg.policy n) (alg₀.policy n) p ar.1) := by
           conv_lhs => rw [← Kernel.withDensity_rnDeriv_eq' (hc.policy n)]
-          exact Kernel.compProd_withDensity_left (Kernel.measurable_rnDeriv _ _)
+          exact Kernel.withDensity_compProd (Kernel.measurable_rnDeriv _ _)
         have h_sf : IsSFiniteKernel ((alg₀.policy n ⊗ₖ env.feedback n).withDensity
             (fun p ar ↦ Kernel.rnDeriv (alg.policy n) (alg₀.policy n) p ar.1)) := by
           rw [← h_inner]
           infer_instance
-        rw [stepKernel_def alg env n, h_inner, Kernel.compProd_withDensity_right (by fun_prop)]
+        rw [stepKernel_def alg env n, h_inner, Kernel.compProd_withDensity (by fun_prop)]
         rfl
       have : IsMarkovKernel ((stepKernel alg₀ env n).withDensity ρ) := by
         rw [← hs]
@@ -160,7 +160,7 @@ lemma hasLaw_history_withDensity (h : IsAlgEnvSeq O A Y alg env P)
       · exact (h₀.measurable_history n).prodMk (h₀.measurable_step n)
       · exact (h.measurable_history n).prodMk (h.measurable_step n)
       rw [(h.hasCondDistrib_step n).map_eq, (h₀.hasCondDistrib_step n).map_eq, ih, hs,
-        Measure.compProd_withDensity_withDensity (by fun_prop) (by fun_prop)]
+        Measure.withDensity_compProd_withDensity (by fun_prop) (by fun_prop)]
       exact map_equiv_withDensity (by fun_prop)
 
 end IsAlgEnvSeq
diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean
index e345f31f..be324371 100644
--- a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean
+++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean
@@ -83,7 +83,7 @@ lemma hasLaw_history_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     have hE₀ := h₀.measurable_param
     rw [← condDistrib_comp_map hE.aemeasurable (by fun_prop), h.hasLaw_env.map_eq,
           Measure.bind_congr_right (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n),
-          Kernel.comp_withDensity_eq_withDensity_comp (by fun_prop),
+          ← Measure.withDensity_comp (by fun_prop),
           ← h₀.hasLaw_env.map_eq, condDistrib_comp_map hE₀.aemeasurable (by fun_prop)]
 
 variable [StandardBorelSpace 𝓔] [Nonempty 𝓔]
@@ -101,13 +101,15 @@ lemma hasCondDistrib_env_history (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     have hY := h.measurable_feedback
     have hA₀ := h₀.measurable_action
     have hY₀ := h₀.measurable_feedback
+    have hE := h.measurable_param
     have hE₀ := h₀.measurable_param
-    rw [← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq,
+    rw [← map_swap_compProd_map_condDistrib (by fun_prop) (by fun_prop), h.hasLaw_env.map_eq,
       Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop)
         (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n),
       map_swap_withDensity_comp_snd (by fun_prop),
-      ← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop),
-      ← compProd_map_condDistrib (by fun_prop), ← Measure.compProd_withDensity_left (by fun_prop),
+      ← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop) (by fun_prop),
+      ← compProd_map_condDistrib (by fun_prop) (by fun_prop),
+      ← Measure.withDensity_compProd (by fun_prop),
       ← (hasLaw_history_withDensity h h₀ hc n).map_eq]
 
 end IsBayesAlgEnvSeq
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
index 65778126..91829c5e 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
@@ -148,8 +148,6 @@ lemma feedback_tendsto_any (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f
   let g : ((Iic n) → 𝓨) → ℝ := fun r ↦ (fun i ↦ dist (r i) (f a)).min
   filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h g] with ω hω
   simp only [eq_iff_iff]
-  change ε ≤ (fun (j : Iic n) ↦ dist (Y j ω) (f a)).min ↔
-    ε ≤ (fun (j : Iic n) ↦ dist (f (A j ω)) (f a)).min
   simp [g, hω]
 
 variable {R : ℕ → Ω → ℝ} {f : 𝓐 → ℝ} (hfc : Continuous f) {a : 𝓐}
diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
index 779a6a71..dd29a648 100644
--- a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
@@ -246,7 +246,7 @@ lemma hasLaw_IT_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
       (condDistrib (trajectory (noObs Ω) A Y) E P e) := by
   rw [← h.hasLaw_env.map_eq, show history (noObs Ω) A Y n
     = IT.hist (𝓞 := Unit) (𝓐 := 𝓐) (𝓨 := 𝓨) n ∘ trajectory (noObs Ω) A Y from rfl]
-  filter_upwards [condDistrib_comp E
+  filter_upwards [condDistrib_comp h.measurable_param.aemeasurable
     (measurable_trajectory (O := noObs Ω) (fun _ ↦ measurable_const) h.measurable_action
       h.measurable_feedback).aemeasurable
     (IT.measurable_hist (𝓞 := Unit) (𝓐 := 𝓐) (𝓨 := 𝓨) n)] with _ he
diff --git a/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean b/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
index a45faebd..3cad44da 100644
--- a/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
+++ b/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
@@ -124,7 +124,7 @@ lemma klDiv_map_trajectory_eq_iSup (hO : ∀ n, Measurable (O n)) (hA : ∀ n, M
     klDiv (P.map (trajectory O A Y)) (P'.map (trajectory O' A' Y')) =
       ⨆ n, klDiv (P.map (history O A Y n)) (P'.map (history O' A' Y' n)) := by
   have hg : ∀ n, Measurable fun f : ℕ → Round 𝓞 𝓐 𝓨 ↦ fun i : Fin n ↦ f i.1 := fun n ↦
-    measurable_pi_lambda _ fun i ↦ measurable_pi_apply i.1
+    .of_eval fun i ↦ measurable_pi_apply i.1
   rw [klDiv_eq_iSup_map hg ?_ MeasurableSpace.iSup_comap_restrictFin]
   · refine iSup_congr fun n ↦ ?_
     rw [Measure.map_map (hg n) (measurable_trajectory hO hA hY),
@@ -136,7 +136,7 @@ lemma klDiv_map_trajectory_eq_iSup (hO : ∀ n, Measurable (O n)) (hA : ∀ n, M
           fun f : ℕ → Round 𝓞 𝓐 𝓨 ↦ fun i : Fin m ↦ f i.1 := rfl
     beta_reduce
     rw [this, ← MeasurableSpace.comap_comp]
-    exact MeasurableSpace.comap_mono (measurable_pi_lambda _ fun i ↦
+    exact MeasurableSpace.comap_mono (Measurable.of_eval fun i ↦
       measurable_pi_apply (Fin.castLE hnm i)).comap_le
 
 /-- **Chain rule for trajectories.** For two algorithms `alg` and `alg'` run against
diff --git a/lake-manifest.json b/lake-manifest.json
index 2eb557e1..a19dda4a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cf65d43b4f5e1a79482e8c488d121853b9d7ca05",
+   "rev": "c02174567c98cac8b9a8e2ee34ee8e2ffa98df94",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "cf65d43b4f5e1a79482e8c488d121853b9d7ca05",
+   "inputRev": "c02174567c98cac8b9a8e2ee34ee8e2ffa98df94",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d8823026ac7ef130c253089d95685f9877b95323",
+   "rev": "1681d78dd6e65e38b143f9740d829c826673807c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d54dddc581e08be364c278052863524bff7a99a9",
+   "rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index be4eda1d..5f3078d8 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -17,7 +17,7 @@ rev = "v4.33.0"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "cf65d43b4f5e1a79482e8c488d121853b9d7ca05"
+rev = "c02174567c98cac8b9a8e2ee34ee8e2ffa98df94"
 
 [[lean_lib]]
 name = "LeanMachineLearning"