Update Mathlib

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⟩) ∘

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

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,

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'

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]

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 η) = κ :=

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]