[Merged by Bors] - feat(Probability/Kernel): disintegration of finite kernels

Mathlib.lean

@@ -3235,11 +3235,13 @@ import Mathlib.Probability.Kernel.Basic
 import Mathlib.Probability.Kernel.Composition
 import Mathlib.Probability.Kernel.CondDistrib
 import Mathlib.Probability.Kernel.Condexp
-import Mathlib.Probability.Kernel.Disintegration
+import Mathlib.Probability.Kernel.Disintegration.Basic
 import Mathlib.Probability.Kernel.Disintegration.CdfToKernel
 import Mathlib.Probability.Kernel.Disintegration.CondCdf
 import Mathlib.Probability.Kernel.Disintegration.Density
+import Mathlib.Probability.Kernel.Disintegration.Integral
 import Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
+import Mathlib.Probability.Kernel.Disintegration.Unique
 import Mathlib.Probability.Kernel.IntegralCompProd
 import Mathlib.Probability.Kernel.Invariance
 import Mathlib.Probability.Kernel.MeasurableIntegral

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -1091,4 +1091,13 @@ theorem exists_measurableEmbedding_real : ∃ f : α → ℝ, MeasurableEmbeddin
   exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩
 #align measure_theory.exists_measurable_embedding_real MeasureTheory.exists_measurableEmbedding_real
 
+/-- A measurable embedding of a standard Borel space into `ℝ`. -/
+noncomputable
+def embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Ω → ℝ :=
+  (exists_measurableEmbedding_real Ω).choose
+
+lemma measurableEmbedding_embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] :
+    MeasurableEmbedding (embeddingReal Ω) :=
+  (exists_measurableEmbedding_real Ω).choose_spec
+
 end MeasureTheory

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -689,6 +689,53 @@ theorem measurable_of_measurable_on_compl_singleton [MeasurableSingletonClass α
 
 end Subtype
 
+section Atoms
+
+variable [MeasurableSpace β]
+
+/-- The *measurable atom* of `x` is the intersection of all the measurable sets countaining `x`.
+It is measurable when the space is countable (or more generally when the measurable space is
+countably generated). -/
+def measurableAtom (x : β) : Set β :=
+  ⋂ (s : Set β) (_h's : x ∈ s) (_hs : MeasurableSet s), s
+
+@[simp] lemma mem_measurableAtom_self (x : β) : x ∈ measurableAtom x := by
+  simp (config := {contextual := true}) [measurableAtom]
+
+lemma mem_of_mem_measurableAtom {x y : β} (h : y ∈ measurableAtom x) {s : Set β}
+    (hs : MeasurableSet s) (hxs : x ∈ s) : y ∈ s := by
+  simp only [measurableAtom, mem_iInter] at h
+  exact h s hxs hs
+
+lemma measurableAtom_subset {s : Set β} {x : β} (hs : MeasurableSet s) (hx : x ∈ s) :
+    measurableAtom x ⊆ s :=
+  iInter₂_subset_of_subset s hx fun ⦃a⦄ ↦ (by simp [hs])
+
+@[simp] lemma measurableAtom_of_measurableSingletonClass [MeasurableSingletonClass β] (x : β) :
+    measurableAtom x = {x} :=
+  Subset.antisymm (measurableAtom_subset (measurableSet_singleton x) rfl) (by simp)
+
+lemma MeasurableSet.measurableAtom_of_countable [Countable β] (x : β) :
+    MeasurableSet (measurableAtom x) := by
+  have : ∀ (y : β), y ∉ measurableAtom x → ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s :=
+    fun y hy ↦ by simpa [measurableAtom] using hy
+  choose! s hs using this
+  have : measurableAtom x = ⋂ (y ∈ (measurableAtom x)ᶜ), s y := by
+    apply Subset.antisymm
+    · intro z hz
+      simp only [mem_iInter, mem_compl_iff]
+      intro i hi
+      show z ∈ s i
+      exact mem_of_mem_measurableAtom hz (hs i hi).1 (hs i hi).2.1
+    · apply compl_subset_compl.1
+      intro z hz
+      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
+      exact ⟨z, hz, (hs z hz).2.2⟩
+  rw [this]
+  exact MeasurableSet.biInter (to_countable (measurableAtom x)ᶜ) (fun i hi ↦ (hs i hi).1)
+
+end Atoms
+
 section Prod
 
 /-- A `MeasurableSpace` structure on the product of two measurable spaces. -/
@@ -813,14 +860,23 @@ instance Prod.instMeasurableSingletonClass
   ⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ .prod (.singleton a) (.singleton b)⟩
 #align prod.measurable_singleton_class Prod.instMeasurableSingletonClass
 
-theorem measurable_from_prod_countable [Countable β] [MeasurableSingletonClass β]
-    {_ : MeasurableSpace γ} {f : α × β → γ} (hf : ∀ y, Measurable fun x => f (x, y)) :
+theorem measurable_from_prod_countable' [Countable β]
+    {_ : MeasurableSpace γ} {f : α × β → γ} (hf : ∀ y, Measurable fun x => f (x, y))
+    (h'f : ∀ y y' x, y' ∈ measurableAtom y → f (x, y') = f (x, y)) :
     Measurable f := fun s hs => by
-  have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ ({y} : Set β) := by
+  have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β) := by
     ext1 ⟨x, y⟩
-    simp [and_assoc, and_left_comm]
+    simp only [mem_preimage, mem_iUnion, mem_prod]
+    refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
+    rintro ⟨y', hy's, hy'⟩
+    rwa [h'f y' y x hy']
   rw [this]
-  exact .iUnion fun y => (hf y hs).prod (.singleton y)
+  exact .iUnion (fun y ↦ (hf y hs).prod (.measurableAtom_of_countable y))
+
+theorem measurable_from_prod_countable [Countable β] [MeasurableSingletonClass β]
+    {_ : MeasurableSpace γ} {f : α × β → γ} (hf : ∀ y, Measurable fun x => f (x, y)) :
+    Measurable f :=
+  measurable_from_prod_countable' hf (by simp (config := {contextual := true}))
 #align measurable_from_prod_countable measurable_from_prod_countable
 
 /-- A piecewise function on countably many pieces is measurable if all the data is measurable. -/

Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

@@ -106,9 +106,23 @@ theorem CountablyGenerated.sup {m₁ m₂ : MeasurableSpace β} (h₁ : @Countab
   rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
   exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩
 
-instance (priority := 100) [MeasurableSpace α] [Finite α] : CountablyGenerated α where
-  isCountablyGenerated :=
-    ⟨{s | MeasurableSet s}, Set.to_countable _, generateFrom_measurableSet.symm⟩
+/-- Any measurable space structure on a countable space is countably generated. -/
+instance (priority := 100) [MeasurableSpace α] [Countable α] : CountablyGenerated α where
+  isCountablyGenerated := by
+    refine ⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩
+    refine le_antisymm ?_ (generateFrom_le (by simp [MeasurableSet.measurableAtom_of_countable]))
+    intro s hs
+    have : s = ⋃ y ∈ s, measurableAtom y := by
+      apply Subset.antisymm
+      · intro x hx
+        simpa using ⟨x, hx, by simp⟩
+      · simp only [iUnion_subset_iff]
+        intro x hx
+        exact measurableAtom_subset hs hx
+    rw [this]
+    apply MeasurableSet.biUnion (to_countable s) (fun x _hx ↦ ?_)
+    apply measurableSet_generateFrom
+    simp
 
 instance [MeasurableSpace α] [CountablyGenerated α] {p : α → Prop} :
     CountablyGenerated { x // p x } := .comap _
@@ -455,4 +469,22 @@ lemma measurableSet_countablePartitionSet (n : ℕ) (a : α) :
     MeasurableSet (countablePartitionSet n a) :=
   measurableSet_countablePartition n (countablePartitionSet_mem n a)
 
+section CountableOrCountablyGenerated
+
+variable [MeasurableSpace β]
+
+/-- A class registering that either `α` is countable or `β` is a countably generated
+measurable space. -/
+class CountableOrCountablyGenerated (α β : Type*) [MeasurableSpace α] [MeasurableSpace β] : Prop :=
+  countableOrCountablyGenerated : Countable α ∨ MeasurableSpace.CountablyGenerated β
+
+instance instCountableOrCountablyGeneratedOfCountable [h1 : Countable α] :
+    CountableOrCountablyGenerated α β := ⟨Or.inl h1⟩
+
+instance instCountableOrCountablyGeneratedOfCountablyGenerated
+    [h : MeasurableSpace.CountablyGenerated β] :
+    CountableOrCountablyGenerated α β := ⟨Or.inr h⟩
+
+end CountableOrCountablyGenerated
+
 end MeasurableSpace

Mathlib/Probability/Kernel/Composition.lean

@@ -583,6 +583,25 @@ lemma compProd_add_right (μ : kernel α β) (κ η : kernel (α × β) γ)
   rw [lintegral_add_left]
   exact measurable_kernel_prod_mk_left' hs a
 
+lemma comapRight_compProd_id_prod {δ : Type*} {mδ : MeasurableSpace δ}
+    (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ) [IsSFiniteKernel η]
+    {f : δ → γ} (hf : MeasurableEmbedding f) :
+    comapRight (κ ⊗ₖ η) (MeasurableEmbedding.id.prod_mk hf) = κ ⊗ₖ (comapRight η hf) := by
+  ext a t ht
+  rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply _ _ _ ht]
+  swap; · exact (MeasurableEmbedding.id.prod_mk hf).measurableSet_image.mpr ht
+  refine lintegral_congr (fun b ↦ ?_)
+  simp only [id_eq, Set.mem_image, Prod.mk.injEq, Prod.exists]
+  rw [comapRight_apply']
+  swap; · exact measurable_prod_mk_left ht
+  congr with x
+  simp only [Set.mem_setOf_eq, Set.mem_image]
+  constructor
+  · rintro ⟨b', c, h, rfl, rfl⟩
+    exact ⟨c, h, rfl⟩
+  · rintro ⟨c, h, rfl⟩
+    exact ⟨b, c, h, rfl, rfl⟩
+
 end CompositionProduct
 
 section MapComap

Mathlib/Probability/Kernel/CondDistrib.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.Probability.Kernel.Disintegration
+import Mathlib.Probability.Kernel.Disintegration.Unique
 import Mathlib.Probability.Notation
 
 #align_import probability.kernel.cond_distrib from "leanprover-community/mathlib"@"00abe0695d8767201e6d008afa22393978bb324d"
@@ -74,7 +74,7 @@ variable {mβ : MeasurableSpace β} {s : Set Ω} {t : Set β} {f : β × Ω →
 lemma condDistrib_apply_of_ne_zero [MeasurableSingletonClass β]
     (hY : Measurable Y) (x : β) (hX : μ.map X {x} ≠ 0) (s : Set Ω) :
     condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s) := by
-  rw [condDistrib, condKernel_apply_of_ne_zero _ s]
+  rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s]
   · rw [Measure.fst_map_prod_mk hY]
   · rwa [Measure.fst_map_prod_mk hY]
 
@@ -125,7 +125,7 @@ theorem condDistrib_ae_eq_of_measure_eq_compProd (hX : Measurable X) (hY : Measu
     rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
     exacts [rfl, Measurable.prod hX hY, measurable_fst hs]
   rw [heq, condDistrib]
-  refine' eq_condKernel_of_measure_eq_compProd _ _ _
+  refine eq_condKernel_of_measure_eq_compProd _ ?_
   convert hκ
   exact heq.symm
 
@@ -202,7 +202,7 @@ theorem set_lintegral_preimage_condDistrib (hX : Measurable X) (hY : AEMeasurabl
   -- (`rw` does not see that the two forms are defeq)
   conv_lhs => arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
   rw [lintegral_comp (kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht, ←
-    Measure.fst_map_prod_mk₀ hY, set_lintegral_condKernel_eq_measure_prod _ ht hs,
+    Measure.fst_map_prod_mk₀ hY, Measure.set_lintegral_condKernel_eq_measure_prod ht hs,
     Measure.map_apply_of_aemeasurable (hX.aemeasurable.prod_mk hY) (ht.prod hs), mk_preimage_prod]
 #align probability_theory.set_lintegral_preimage_cond_distrib ProbabilityTheory.set_lintegral_preimage_condDistrib
 
@@ -248,7 +248,7 @@ theorem condexp_prod_ae_eq_integral_condDistrib' [NormedSpace ℝ F] [CompleteSp
     · rw [← Measure.restrict_map hX ht]
       exact (hf_int.1.integral_condDistrib_map hY).restrict
     rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prod_mk₀ hY, condDistrib,
-      set_integral_condKernel_univ_right ht hf_int.integrableOn,
+      Measure.set_integral_condKernel_univ_right ht hf_int.integrableOn,
       set_integral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prod_mk hY),
       mk_preimage_prod, preimage_univ, inter_univ]
   · exact aestronglyMeasurable'_integral_condDistrib hX.aemeasurable hY hf_int.1

Mathlib/Probability/Kernel/Condexp.lean

@@ -97,15 +97,15 @@ theorem stronglyMeasurable_condexpKernel {s : Set Ω} (hs : MeasurableSet s) :
   Measurable.stronglyMeasurable (measurable_condexpKernel hs)
 
 theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condexpKernel [NormedSpace ℝ F]
-    [CompleteSpace F] (hf : AEStronglyMeasurable f μ) :
+    (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable (fun ω => ∫ y, f y ∂condexpKernel μ m ω) μ := by
   simp_rw [condexpKernel_apply_eq_condDistrib]
   exact AEStronglyMeasurable.integral_condDistrib
     (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
     (hf.comp_snd_map_prod_id inf_le_right)
 #align measure_theory.ae_strongly_measurable.integral_condexp_kernel MeasureTheory.AEStronglyMeasurable.integral_condexpKernel
 
-theorem aestronglyMeasurable'_integral_condexpKernel [NormedSpace ℝ F] [CompleteSpace F]
+theorem aestronglyMeasurable'_integral_condexpKernel [NormedSpace ℝ F]
     (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable' m (fun ω => ∫ y, f y ∂condexpKernel μ m ω) μ := by
   rw [condexpKernel]
@@ -139,15 +139,15 @@ theorem _root_.MeasureTheory.Integrable.integral_norm_condexpKernel (hf_int : In
 #align measure_theory.integrable.integral_norm_condexp_kernel MeasureTheory.Integrable.integral_norm_condexpKernel
 
 theorem _root_.MeasureTheory.Integrable.norm_integral_condexpKernel [NormedSpace ℝ F]
-    [CompleteSpace F] (hf_int : Integrable f μ) :
+    (hf_int : Integrable f μ) :
     Integrable (fun ω => ‖∫ y, f y ∂condexpKernel μ m ω‖) μ := by
   rw [condexpKernel]
   exact Integrable.norm_integral_condDistrib
     (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
     (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
 #align measure_theory.integrable.norm_integral_condexp_kernel MeasureTheory.Integrable.norm_integral_condexpKernel
 
-theorem _root_.MeasureTheory.Integrable.integral_condexpKernel [NormedSpace ℝ F] [CompleteSpace F]
+theorem _root_.MeasureTheory.Integrable.integral_condexpKernel [NormedSpace ℝ F]
     (hf_int : Integrable f μ) :
     Integrable (fun ω => ∫ y, f y ∂condexpKernel μ m ω) μ := by
   rw [condexpKernel]