diff --git a/Mathlib.lean b/Mathlib.lean index 545e64b2cc298..e2498af62f0aa 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Constructions/Polish.lean b/Mathlib/MeasureTheory/Constructions/Polish.lean index b3c43cca0fef6..e899700457038 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean index 7ec688daa3ae2..6ae658cfc751c 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean +++ b/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. -/ diff --git a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean index dadb3ec19c6aa..c147258133198 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean +++ b/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 diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index cec800f3067aa..b4c0dbddbaef8 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/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 diff --git a/Mathlib/Probability/Kernel/CondDistrib.lean b/Mathlib/Probability/Kernel/CondDistrib.lean index 3494962fb3c4c..d856907837bac 100644 --- a/Mathlib/Probability/Kernel/CondDistrib.lean +++ b/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 diff --git a/Mathlib/Probability/Kernel/Condexp.lean b/Mathlib/Probability/Kernel/Condexp.lean index cc85bbb99c7d5..870f9b8eff29b 100644 --- a/Mathlib/Probability/Kernel/Condexp.lean +++ b/Mathlib/Probability/Kernel/Condexp.lean @@ -97,7 +97,7 @@ 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 @@ -105,7 +105,7 @@ theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condexpKernel [Normed (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,7 +139,7 @@ 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 @@ -147,7 +147,7 @@ theorem _root_.MeasureTheory.Integrable.norm_integral_condexpKernel [NormedSpace (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] diff --git a/Mathlib/Probability/Kernel/Disintegration.lean b/Mathlib/Probability/Kernel/Disintegration.lean deleted file mode 100644 index 49f25ab2436da..0000000000000 --- a/Mathlib/Probability/Kernel/Disintegration.lean +++ /dev/null @@ -1,657 +0,0 @@ -/- -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, Kexing Ying --/ -import Mathlib.Probability.Kernel.Disintegration.CondCdf -import Mathlib.MeasureTheory.Constructions.Polish -import Mathlib.Probability.Kernel.MeasureCompProd - -#align_import probability.kernel.disintegration from "leanprover-community/mathlib"@"6315581f5650ffa2fbdbbbedc41243c8d7070981" - -/-! -# Disintegration of measures on product spaces - -Let `ρ` be a finite measure on `α × Ω`, where `Ω` is a standard Borel space. In mathlib terms, `Ω` -verifies `[Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω]`. -Then there exists a kernel `ρ.condKernel : kernel α Ω` such that for any measurable set -`s : Set (α × Ω)`, `ρ s = ∫⁻ a, ρ.condKernel a {x | (a, x) ∈ s} ∂ρ.fst`. - -In terms of kernels, `ρ.condKernel` is such that for any measurable space `γ`, we -have a disintegration of the constant kernel from `γ` with value `ρ`: -`kernel.const γ ρ = (kernel.const γ ρ.fst) ⊗ₖ (kernel.prodMkLeft γ (condKernel ρ))`, -where `ρ.fst` is the marginal measure of `ρ` on `α`. In particular, `ρ = ρ.fst ⊗ₘ ρ.condKernel`. - -In order to obtain a disintegration for any standard Borel space, we use that these spaces embed -measurably into `ℝ`: it then suffices to define a suitable kernel for `Ω = ℝ`. In the real case, -we define a conditional kernel by taking for each `a : α` the measure associated to the Stieltjes -function `condCDF ρ a` (the conditional cumulative distribution function). - -## Main definitions - -* `MeasureTheory.Measure.condKernel ρ : kernel α Ω`: conditional kernel described above. - -## Main statements - -* `ProbabilityTheory.lintegral_condKernel`: - `∫⁻ a, ∫⁻ ω, f (a, ω) ∂(ρ.condKernel a) ∂ρ.fst = ∫⁻ x, f x ∂ρ` -* `ProbabilityTheory.lintegral_condKernel_mem`: - `∫⁻ a, ρ.condKernel a {x | (a, x) ∈ s} ∂ρ.fst = ρ s` -* `ProbabilityTheory.kernel.const_eq_compProd`: - `kernel.const γ ρ = (kernel.const γ ρ.fst) ⊗ₖ (kernel.prodMkLeft γ ρ.condKernel)` -* `ProbabilityTheory.measure_eq_compProd`: `ρ = ρ.fst ⊗ₘ ρ.condKernel` -* `ProbabilityTheory.eq_condKernel_of_measure_eq_compProd`: a.e. uniqueness of `condKernel` - --/ - - -open MeasureTheory Set Filter - -open scoped ENNReal MeasureTheory Topology ProbabilityTheory - -namespace ProbabilityTheory - -variable {α : Type*} {mα : MeasurableSpace α} - -section Real - -/-! ### Disintegration of measures on `α × ℝ` -/ - - -/-- Conditional measure on the second space of the product given the value on the first, as a -kernel. Use the more general `condKernel`. -/ -noncomputable def condKernelReal (ρ : Measure (α × ℝ)) : kernel α ℝ where - val a := (condCDF ρ a).measure - property := measurable_measure_condCDF ρ -#align probability_theory.cond_kernel_real ProbabilityTheory.condKernelReal - -instance (ρ : Measure (α × ℝ)) : IsMarkovKernel (condKernelReal ρ) := - ⟨fun a => by rw [condKernelReal]; exact instIsProbabilityMeasureCondCDF ρ a⟩ - -theorem condKernelReal_Iic (ρ : Measure (α × ℝ)) (a : α) (x : ℝ) : - condKernelReal ρ a (Iic x) = ENNReal.ofReal (condCDF ρ a x) := - measure_condCDF_Iic ρ a x -#align probability_theory.cond_kernel_real_Iic ProbabilityTheory.condKernelReal_Iic - -theorem set_lintegral_condKernelReal_Iic (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℝ) - {s : Set α} (hs : MeasurableSet s) : - ∫⁻ a in s, condKernelReal ρ a (Iic x) ∂ρ.fst = ρ (s ×ˢ Iic x) := by - simp_rw [condKernelReal_Iic]; exact set_lintegral_condCDF ρ x hs -#align probability_theory.set_lintegral_cond_kernel_real_Iic ProbabilityTheory.set_lintegral_condKernelReal_Iic - -theorem set_lintegral_condKernelReal_univ (ρ : Measure (α × ℝ)) {s : Set α} (hs : MeasurableSet s) : - ∫⁻ a in s, condKernelReal ρ a univ ∂ρ.fst = ρ (s ×ˢ univ) := by - simp only [measure_univ, lintegral_const, Measure.restrict_apply, MeasurableSet.univ, univ_inter, - one_mul, Measure.fst_apply hs, ← prod_univ] -#align probability_theory.set_lintegral_cond_kernel_real_univ ProbabilityTheory.set_lintegral_condKernelReal_univ - -theorem lintegral_condKernelReal_univ (ρ : Measure (α × ℝ)) : - ∫⁻ a, condKernelReal ρ a univ ∂ρ.fst = ρ univ := by - rw [← set_lintegral_univ, set_lintegral_condKernelReal_univ ρ MeasurableSet.univ, - univ_prod_univ] -#align probability_theory.lintegral_cond_kernel_real_univ ProbabilityTheory.lintegral_condKernelReal_univ - -variable (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] - -theorem set_lintegral_condKernelReal_prod {s : Set α} (hs : MeasurableSet s) {t : Set ℝ} - (ht : MeasurableSet t) : ∫⁻ a in s, condKernelReal ρ a t ∂ρ.fst = ρ (s ×ˢ t) := by - -- `set_lintegral_condKernelReal_Iic` gives the result for `t = Iic x`. These sets form a - -- π-system that generates the Borel σ-algebra, hence we can get the same equality for any - -- measurable set `t`. - apply MeasurableSpace.induction_on_inter (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic _ _ _ _ ht - · simp only [measure_empty, lintegral_const, zero_mul, prod_empty] - · rintro t ⟨q, rfl⟩ - exact set_lintegral_condKernelReal_Iic ρ q hs - · intro t ht ht_lintegral - calc - ∫⁻ a in s, condKernelReal ρ a tᶜ ∂ρ.fst = - ∫⁻ a in s, condKernelReal ρ a univ - condKernelReal ρ a t ∂ρ.fst := by - congr with a; rw [measure_compl ht (measure_ne_top (condKernelReal ρ a) _)] - _ = ∫⁻ a in s, condKernelReal ρ a univ ∂ρ.fst - ∫⁻ a in s, condKernelReal ρ a t ∂ρ.fst := by - rw [lintegral_sub (kernel.measurable_coe (condKernelReal ρ) ht)] - · rw [ht_lintegral] - exact measure_ne_top ρ _ - · exact eventually_of_forall fun a => measure_mono (subset_univ _) - _ = ρ (s ×ˢ univ) - ρ (s ×ˢ t) := by - rw [set_lintegral_condKernelReal_univ ρ hs, ht_lintegral] - _ = ρ (s ×ˢ tᶜ) := by - rw [← measure_diff _ (hs.prod ht) (measure_ne_top ρ _)] - · rw [prod_diff_prod, compl_eq_univ_diff] - simp only [diff_self, empty_prod, union_empty] - · rw [prod_subset_prod_iff] - exact Or.inl ⟨subset_rfl, subset_univ t⟩ - · intro f hf_disj hf_meas hf_eq - simp_rw [measure_iUnion hf_disj hf_meas] - rw [lintegral_tsum fun i => (kernel.measurable_coe _ (hf_meas i)).aemeasurable.restrict, - prod_iUnion, measure_iUnion] - · simp_rw [hf_eq] - · intro i j hij - rw [Function.onFun, Set.disjoint_prod] - exact Or.inr (hf_disj hij) - · exact fun i => MeasurableSet.prod hs (hf_meas i) -#align probability_theory.set_lintegral_cond_kernel_real_prod ProbabilityTheory.set_lintegral_condKernelReal_prod - -theorem lintegral_condKernelReal_mem {s : Set (α × ℝ)} (hs : MeasurableSet s) : - ∫⁻ a, condKernelReal ρ a {x | (a, x) ∈ s} ∂ρ.fst = ρ s := by - -- `set_lintegral_condKernelReal_prod` gives the result for sets of the form `t₁ × t₂`. These - -- sets form a π-system that generates the product σ-algebra, hence we can get the same equality - -- for any measurable set `s`. - apply MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod _ _ _ _ hs - · simp only [mem_empty_iff_false, setOf_false, measure_empty, lintegral_const, - zero_mul] - · rintro _ ⟨t₁, ht₁, t₂, ht₂, rfl⟩ - have h_prod_eq_snd : ∀ a ∈ t₁, {x : ℝ | (a, x) ∈ t₁ ×ˢ t₂} = t₂ := by - intro a ha - simp only [ha, prod_mk_mem_set_prod_eq, true_and_iff, setOf_mem_eq] - rw [← lintegral_add_compl _ ht₁] - have h_eq1 : ∫⁻ a in t₁, condKernelReal ρ a {x : ℝ | (a, x) ∈ t₁ ×ˢ t₂} ∂ρ.fst = - ∫⁻ a in t₁, condKernelReal ρ a t₂ ∂ρ.fst := by - refine' set_lintegral_congr_fun ht₁ (eventually_of_forall fun a ha => _) - rw [h_prod_eq_snd a ha] - have h_eq2 : ∫⁻ a in t₁ᶜ, condKernelReal ρ a {x : ℝ | (a, x) ∈ t₁ ×ˢ t₂} ∂ρ.fst = 0 := by - suffices h_eq_zero : ∀ a ∈ t₁ᶜ, condKernelReal ρ a {x : ℝ | (a, x) ∈ t₁ ×ˢ t₂} = 0 by - rw [set_lintegral_congr_fun ht₁.compl (eventually_of_forall h_eq_zero)] - simp only [lintegral_const, zero_mul] - intro a hat₁ - rw [mem_compl_iff] at hat₁ - simp only [hat₁, prod_mk_mem_set_prod_eq, false_and_iff, setOf_false, measure_empty] - rw [h_eq1, h_eq2, add_zero] - exact set_lintegral_condKernelReal_prod ρ ht₁ ht₂ - · intro t ht ht_eq - calc - ∫⁻ a, condKernelReal ρ a {x : ℝ | (a, x) ∈ tᶜ} ∂ρ.fst = - ∫⁻ a, condKernelReal ρ a {x : ℝ | (a, x) ∈ t}ᶜ ∂ρ.fst := rfl - _ = ∫⁻ a, condKernelReal ρ a univ - condKernelReal ρ a {x : ℝ | (a, x) ∈ t} ∂ρ.fst := by - congr with a : 1 - exact measure_compl (measurable_prod_mk_left ht) (measure_ne_top (condKernelReal ρ a) _) - _ = ∫⁻ a, condKernelReal ρ a univ ∂ρ.fst - - ∫⁻ a, condKernelReal ρ a {x : ℝ | (a, x) ∈ t} ∂ρ.fst := by - have h_le : (fun a => condKernelReal ρ a {x : ℝ | (a, x) ∈ t}) ≤ᵐ[ρ.fst] fun a => - condKernelReal ρ a univ := eventually_of_forall fun a => measure_mono (subset_univ _) - rw [lintegral_sub _ _ h_le] - · exact kernel.measurable_kernel_prod_mk_left ht - refine' ((lintegral_mono_ae h_le).trans_lt _).ne - rw [lintegral_condKernelReal_univ] - exact measure_lt_top ρ univ - _ = ρ univ - ρ t := by rw [ht_eq, lintegral_condKernelReal_univ] - _ = ρ tᶜ := (measure_compl ht (measure_ne_top _ _)).symm - · intro f hf_disj hf_meas hf_eq - have h_eq : ∀ a, {x | (a, x) ∈ ⋃ i, f i} = ⋃ i, {x | (a, x) ∈ f i} := by - intro a - ext1 x - simp only [mem_iUnion, mem_setOf_eq] - simp_rw [h_eq] - have h_disj : ∀ a, Pairwise (Disjoint on fun i => {x | (a, x) ∈ f i}) := by - intro a i j hij - have h_disj := hf_disj hij - rw [Function.onFun, disjoint_iff_inter_eq_empty] at h_disj ⊢ - ext1 x - simp only [mem_inter_iff, mem_setOf_eq, mem_empty_iff_false, iff_false_iff] - intro h_mem_both - suffices (a, x) ∈ ∅ by rwa [mem_empty_iff_false] at this - rwa [← h_disj, mem_inter_iff] - calc - ∫⁻ a, condKernelReal ρ a (⋃ i, {x | (a, x) ∈ f i}) ∂ρ.fst = - ∫⁻ a, ∑' i, condKernelReal ρ a {x | (a, x) ∈ f i} ∂ρ.fst := by - congr with a : 1 - rw [measure_iUnion (h_disj a) fun i => measurable_prod_mk_left (hf_meas i)] - _ = ∑' i, ∫⁻ a, condKernelReal ρ a {x | (a, x) ∈ f i} ∂ρ.fst := - (lintegral_tsum fun i => (kernel.measurable_kernel_prod_mk_left (hf_meas i)).aemeasurable) - _ = ∑' i, ρ (f i) := by simp_rw [hf_eq] - _ = ρ (iUnion f) := (measure_iUnion hf_disj hf_meas).symm -#align probability_theory.lintegral_cond_kernel_real_mem ProbabilityTheory.lintegral_condKernelReal_mem - -theorem kernel.const_eq_compProd_real (γ : Type*) [MeasurableSpace γ] (ρ : Measure (α × ℝ)) - [IsFiniteMeasure ρ] : - kernel.const γ ρ = kernel.const γ ρ.fst ⊗ₖ kernel.prodMkLeft γ (condKernelReal ρ) := by - ext a s hs : 2 - rw [kernel.compProd_apply _ _ _ hs, kernel.const_apply, kernel.const_apply] - simp_rw [kernel.prodMkLeft_apply] - rw [lintegral_condKernelReal_mem ρ hs] -#align probability_theory.kernel.const_eq_comp_prod_real ProbabilityTheory.kernel.const_eq_compProd_real - -theorem measure_eq_compProd_real : ρ = ρ.fst ⊗ₘ condKernelReal ρ := by - rw [Measure.compProd, ← kernel.const_eq_compProd_real Unit ρ, kernel.const_apply] -#align probability_theory.measure_eq_comp_prod_real ProbabilityTheory.measure_eq_compProd_real - -theorem lintegral_condKernelReal {f : α × ℝ → ℝ≥0∞} (hf : Measurable f) : - ∫⁻ a, ∫⁻ y, f (a, y) ∂condKernelReal ρ a ∂ρ.fst = ∫⁻ x, f x ∂ρ := by - nth_rw 3 [measure_eq_compProd_real ρ] - rw [Measure.lintegral_compProd hf] -#align probability_theory.lintegral_cond_kernel_real ProbabilityTheory.lintegral_condKernelReal - -theorem ae_condKernelReal_eq_one {s : Set ℝ} (hs : MeasurableSet s) (hρ : ρ {x | x.snd ∈ sᶜ} = 0) : - ∀ᵐ a ∂ρ.fst, condKernelReal ρ a s = 1 := by - have h : ρ {x | x.snd ∈ sᶜ} = (ρ.fst ⊗ₘ condKernelReal ρ) {x | x.snd ∈ sᶜ} := by - rw [← measure_eq_compProd_real] - rw [hρ, Measure.compProd_apply] at h - swap; · exact measurable_snd hs.compl - rw [eq_comm, lintegral_eq_zero_iff] at h - swap - · simp only [mem_compl_iff, mem_setOf_eq] - exact kernel.measurable_coe _ hs.compl - simp only [mem_compl_iff, mem_setOf_eq, kernel.prodMkLeft_apply'] at h - filter_upwards [h] with a ha - change condKernelReal ρ a sᶜ = 0 at ha - rwa [prob_compl_eq_zero_iff hs] at ha -#align probability_theory.ae_cond_kernel_real_eq_one ProbabilityTheory.ae_condKernelReal_eq_one - -end Real - -section StandardBorel - -/-! ### Disintegration of measures on standard Borel spaces - -Since every standard Borel space embeds measurably into `ℝ`, we can generalize the disintegration -property on `ℝ` to all these spaces. -/ - - -variable {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] - [Nonempty Ω] (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] - -/-- Existence of a conditional kernel. Use the definition `condKernel` to get that kernel. -/ -theorem exists_cond_kernel (γ : Type*) [MeasurableSpace γ] : - ∃ (η : kernel α Ω) (_h : IsMarkovKernel η), kernel.const γ ρ = - (kernel.const γ ρ.fst) ⊗ₖ (kernel.prodMkLeft γ η) := by - obtain ⟨f, hf⟩ := exists_measurableEmbedding_real Ω - let ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f) - -- The general idea is to define `η = kernel.comapRight (condKernelReal ρ') hf`. There is - -- however an issue: that `η` may not be a Markov kernel since its value is only a - -- probability distribution almost everywhere with respect to `ρ.fst`, not everywhere. - -- We modify it to obtain a Markov kernel which is almost everywhere equal. - let ρ_set := (toMeasurable ρ.fst {a | condKernelReal ρ' a (range f) = 1}ᶜ)ᶜ - have hm : MeasurableSet ρ_set := (measurableSet_toMeasurable _ _).compl - have h_eq_one_of_mem : ∀ a ∈ ρ_set, condKernelReal ρ' a (range f) = 1 := by - intro a ha - rw [mem_compl_iff] at ha - have h_ss := subset_toMeasurable ρ.fst {a : α | condKernelReal ρ' a (range f) = 1}ᶜ - suffices ha' : a ∉ {a : α | condKernelReal ρ' a (range f) = 1}ᶜ by - rwa [not_mem_compl_iff] at ha' - exact not_mem_subset h_ss ha - have h_prod_embed : MeasurableEmbedding (Prod.map (id : α → α) f) := - MeasurableEmbedding.id.prod_mk hf - have h_fst : ρ'.fst = ρ.fst := by - ext1 u hu - rw [Measure.fst_apply hu, Measure.fst_apply hu, - Measure.map_apply h_prod_embed.measurable (measurable_fst hu)] - rfl - have h_ae : ∀ᵐ a ∂ρ.fst, a ∈ ρ_set := by - rw [ae_iff] - simp only [ρ_set, not_mem_compl_iff, setOf_mem_eq, measure_toMeasurable] - change ρ.fst {a : α | a ∉ {a' : α | condKernelReal ρ' a' (range f) = 1}} = 0 - rw [← ae_iff, ← h_fst] - refine' ae_condKernelReal_eq_one ρ' hf.measurableSet_range _ - rw [Measure.map_apply h_prod_embed.measurable] - swap; · exact measurable_snd hf.measurableSet_range.compl - convert measure_empty (α := α × Ω) - ext1 x - simp only [mem_compl_iff, mem_range, preimage_setOf_eq, Prod_map, mem_setOf_eq, - mem_empty_iff_false, iff_false_iff, Classical.not_not, exists_apply_eq_apply] - classical - obtain ⟨x₀, hx₀⟩ : ∃ x, x ∈ range f := range_nonempty _ - let η' := - kernel.piecewise hm (condKernelReal ρ') (kernel.deterministic (fun _ => x₀) measurable_const) - -- We show that `kernel.comapRight η' hf` is a suitable Markov kernel. - refine' ⟨kernel.comapRight η' hf, _, _⟩ - · refine' kernel.IsMarkovKernel.comapRight _ _ fun a => _ - rw [kernel.piecewise_apply'] - split_ifs with h_mem - · exact h_eq_one_of_mem _ h_mem - · rw [kernel.deterministic_apply' _ _ hf.measurableSet_range, Set.indicator_apply, if_pos hx₀] - have : kernel.const γ ρ = kernel.comapRight (kernel.const γ ρ') h_prod_embed := by - ext c t ht : 2 - rw [kernel.const_apply, kernel.comapRight_apply' _ _ _ ht, kernel.const_apply, - Measure.map_apply h_prod_embed.measurable (h_prod_embed.measurableSet_image.mpr ht)] - congr with x : 1 - rw [← @Prod.mk.eta _ _ x] - simp only [id, mem_preimage, Prod.map_mk, mem_image, Prod.mk.inj_iff, Prod.exists] - refine' ⟨fun h => ⟨x.1, x.2, h, rfl, rfl⟩, _⟩ - rintro ⟨a, b, h_mem, rfl, hf_eq⟩ - rwa [hf.injective hf_eq] at h_mem - rw [this, kernel.const_eq_compProd_real _ ρ'] - ext c t ht : 2 - rw [kernel.comapRight_apply' _ _ _ ht, - kernel.compProd_apply _ _ _ (h_prod_embed.measurableSet_image.mpr ht), kernel.const_apply, - h_fst, kernel.compProd_apply _ _ _ ht, kernel.const_apply] - refine' lintegral_congr_ae _ - filter_upwards [h_ae] with a ha - rw [kernel.prodMkLeft_apply', kernel.prodMkLeft_apply', kernel.comapRight_apply'] - swap - · exact measurable_prod_mk_left ht - have h1 : {c : ℝ | (a, c) ∈ Prod.map id f '' t} = f '' {c : Ω | (a, c) ∈ t} := by - ext1 x - simp only [Prod_map, id, mem_image, Prod.mk.inj_iff, Prod.exists, mem_setOf_eq] - constructor - · rintro ⟨a', b, h_mem, rfl, hf_eq⟩ - exact ⟨b, h_mem, hf_eq⟩ - · rintro ⟨b, h_mem, hf_eq⟩ - exact ⟨a, b, h_mem, rfl, hf_eq⟩ - have h2 : condKernelReal ρ' (c, a).snd = η' (c, a).snd := by - rw [kernel.piecewise_apply, if_pos ha] - rw [h1, h2] -#align probability_theory.exists_cond_kernel ProbabilityTheory.exists_cond_kernel - -/-- Conditional kernel of a measure on a product space: a Markov kernel such that -`ρ = ρ.fst ⊗ₘ ρ.condKernel` (see `ProbabilityTheory.measure_eq_compProd`). -/ -noncomputable irreducible_def _root_.MeasureTheory.Measure.condKernel : kernel α Ω := - (exists_cond_kernel ρ Unit).choose -#align measure_theory.measure.cond_kernel MeasureTheory.Measure.condKernel - -theorem condKernel_def : ρ.condKernel = (exists_cond_kernel ρ Unit).choose := by - rw [MeasureTheory.Measure.condKernel] -#align probability_theory.cond_kernel_def ProbabilityTheory.condKernel_def - -instance : IsMarkovKernel ρ.condKernel := by - rw [condKernel_def]; exact (exists_cond_kernel ρ Unit).choose_spec.choose - -theorem kernel.const_unit_eq_compProd : - kernel.const Unit ρ = kernel.const Unit ρ.fst ⊗ₖ kernel.prodMkLeft Unit ρ.condKernel := by - simp_rw [condKernel_def]; exact (exists_cond_kernel ρ Unit).choose_spec.choose_spec -#align probability_theory.kernel.const_unit_eq_comp_prod ProbabilityTheory.kernel.const_unit_eq_compProd - -/-- **Disintegration** of finite product measures on `α × Ω`, where `Ω` is standard Borel. Such a -measure can be written as the composition-product of the constant kernel with value `ρ.fst` -(marginal measure over `α`) and a Markov kernel from `α` to `Ω`. We call that Markov kernel -`ProbabilityTheory.condKernel ρ`. -/ -theorem measure_eq_compProd : ρ = ρ.fst ⊗ₘ ρ.condKernel := by - rw [Measure.compProd, ← kernel.const_unit_eq_compProd, kernel.const_apply] -#align probability_theory.measure_eq_comp_prod ProbabilityTheory.measure_eq_compProd - -/-- **Disintegration** of constant kernels. A constant kernel on a product space `α × Ω`, where `Ω` -is standard Borel, can be written as the composition-product of the constant kernel with -value `ρ.fst` (marginal measure over `α`) and a Markov kernel from `α` to `Ω`. We call that -Markov kernel `ProbabilityTheory.condKernel ρ`. -/ -theorem kernel.const_eq_compProd (γ : Type*) [MeasurableSpace γ] (ρ : Measure (α × Ω)) - [IsFiniteMeasure ρ] : - kernel.const γ ρ = kernel.const γ ρ.fst ⊗ₖ kernel.prodMkLeft γ ρ.condKernel := by - ext a s hs : 2 - simpa only [kernel.const_apply, kernel.compProd_apply _ _ _ hs, kernel.prodMkLeft_apply'] using - kernel.ext_iff'.mp (kernel.const_unit_eq_compProd ρ) () s hs -#align probability_theory.kernel.const_eq_comp_prod ProbabilityTheory.kernel.const_eq_compProd - -/-- Auxiliary lemma for `condKernel_apply_of_ne_zero`. -/ -lemma condKernel_apply_of_ne_zero_of_measurableSet [MeasurableSingletonClass α] - {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] - {x : α} (hx : ρ.fst {x} ≠ 0) {s : Set Ω} (hs : MeasurableSet s) : - ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) := by - nth_rewrite 3 [measure_eq_compProd ρ] - rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))] - classical - have : ∀ a, ρ.condKernel a (Prod.mk a ⁻¹' {x} ×ˢ s) - = ({x} : Set α).indicator (fun a ↦ ρ.condKernel a s) a := by - intro a - by_cases hax : a = x - · simp only [hax, Set.singleton_prod, Set.mem_singleton_iff, Set.indicator_of_mem] - congr with y - simp - · simp only [Set.singleton_prod, Set.mem_singleton_iff, hax, not_false_eq_true, - Set.indicator_of_not_mem] - have : Prod.mk a ⁻¹' (Prod.mk x '' s) = ∅ := by - ext y - simp [Ne.symm hax] - simp only [this, measure_empty] - simp_rw [this] - rw [MeasureTheory.lintegral_indicator _ (measurableSet_singleton x)] - simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac] - rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top ρ.fst _), one_mul] - -/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`, -`ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` . -/ -lemma condKernel_apply_of_ne_zero [MeasurableSingletonClass α] - {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {x : α} (hx : ρ.fst {x} ≠ 0) - (s : Set Ω) : - ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) := by - have : ρ.condKernel x s = ((ρ.fst {x})⁻¹ • ρ).comap (fun (y : Ω) ↦ (x, y)) s := by - congr 2 with s hs - simp [condKernel_apply_of_ne_zero_of_measurableSet hx hs, - (measurableEmbedding_prod_mk_left x).comap_apply] - simp [this, (measurableEmbedding_prod_mk_left x).comap_apply, hx] - -theorem lintegral_condKernel_mem {s : Set (α × Ω)} (hs : MeasurableSet s) : - ∫⁻ a, ρ.condKernel a {x | (a, x) ∈ s} ∂ρ.fst = ρ s := by - conv_rhs => rw [measure_eq_compProd ρ] - simp_rw [Measure.compProd_apply hs] - rfl -#align probability_theory.lintegral_cond_kernel_mem ProbabilityTheory.lintegral_condKernel_mem - -theorem set_lintegral_condKernel_eq_measure_prod {s : Set α} (hs : MeasurableSet s) {t : Set Ω} - (ht : MeasurableSet t) : ∫⁻ a in s, ρ.condKernel a t ∂ρ.fst = ρ (s ×ˢ t) := by - have : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t) := by - congr; exact measure_eq_compProd ρ - rw [this, Measure.compProd_apply (hs.prod ht)] - classical - have : ∀ a, ρ.condKernel a (Prod.mk a ⁻¹' s ×ˢ t) - = s.indicator (fun a ↦ ρ.condKernel a t) a := by - intro a - by_cases ha : a ∈ s <;> simp [ha] - simp_rw [this] - rw [lintegral_indicator _ hs] -#align probability_theory.set_lintegral_cond_kernel_eq_measure_prod ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod - -theorem lintegral_condKernel {f : α × Ω → ℝ≥0∞} (hf : Measurable f) : - ∫⁻ a, ∫⁻ ω, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫⁻ x, f x ∂ρ := by - conv_rhs => rw [measure_eq_compProd ρ] - rw [Measure.lintegral_compProd hf] -#align probability_theory.lintegral_cond_kernel ProbabilityTheory.lintegral_condKernel - -theorem set_lintegral_condKernel {f : α × Ω → ℝ≥0∞} (hf : Measurable f) {s : Set α} - (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : - ∫⁻ a in s, ∫⁻ ω in t, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫⁻ x in s ×ˢ t, f x ∂ρ := by - conv_rhs => rw [measure_eq_compProd ρ] - rw [Measure.set_lintegral_compProd hf hs ht] -#align probability_theory.set_lintegral_cond_kernel ProbabilityTheory.set_lintegral_condKernel - -theorem set_lintegral_condKernel_univ_right {f : α × Ω → ℝ≥0∞} (hf : Measurable f) {s : Set α} - (hs : MeasurableSet s) : - ∫⁻ a in s, ∫⁻ ω, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫⁻ x in s ×ˢ univ, f x ∂ρ := by - rw [← set_lintegral_condKernel ρ hf hs MeasurableSet.univ]; simp_rw [Measure.restrict_univ] -#align probability_theory.set_lintegral_cond_kernel_univ_right ProbabilityTheory.set_lintegral_condKernel_univ_right - -theorem set_lintegral_condKernel_univ_left {f : α × Ω → ℝ≥0∞} (hf : Measurable f) {t : Set Ω} - (ht : MeasurableSet t) : - ∫⁻ a, ∫⁻ ω in t, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫⁻ x in univ ×ˢ t, f x ∂ρ := by - rw [← set_lintegral_condKernel ρ hf MeasurableSet.univ ht]; simp_rw [Measure.restrict_univ] -#align probability_theory.set_lintegral_cond_kernel_univ_left ProbabilityTheory.set_lintegral_condKernel_univ_left - -section IntegralCondKernel - -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] - -theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condKernel {ρ : Measure (α × Ω)} - [IsFiniteMeasure ρ] {f : α × Ω → E} (hf : AEStronglyMeasurable f ρ) : - AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst := by - rw [measure_eq_compProd ρ] at hf - exact AEStronglyMeasurable.integral_kernel_compProd hf -#align measure_theory.ae_strongly_measurable.integral_cond_kernel MeasureTheory.AEStronglyMeasurable.integral_condKernel - -theorem integral_condKernel {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → E} - (hf : Integrable f ρ) : ∫ a, ∫ x, f (a, x) ∂ρ.condKernel a ∂ρ.fst = ∫ ω, f ω ∂ρ := by - conv_rhs => rw [measure_eq_compProd ρ] - have hf': Integrable f (ρ.fst ⊗ₘ ρ.condKernel) := by rwa [measure_eq_compProd ρ] at hf - rw [Measure.integral_compProd hf'] -#align probability_theory.integral_cond_kernel ProbabilityTheory.integral_condKernel - -theorem set_integral_condKernel {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → E} - {s : Set α} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) - (hf : IntegrableOn f (s ×ˢ t) ρ) : - ∫ a in s, ∫ ω in t, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ := by - conv_rhs => rw [measure_eq_compProd ρ] - rw [Measure.set_integral_compProd hs ht] - rwa [measure_eq_compProd ρ] at hf -#align probability_theory.set_integral_cond_kernel ProbabilityTheory.set_integral_condKernel - -theorem set_integral_condKernel_univ_right {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → E} - {s : Set α} (hs : MeasurableSet s) (hf : IntegrableOn f (s ×ˢ univ) ρ) : - ∫ a in s, ∫ ω, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫ x in s ×ˢ univ, f x ∂ρ := by - rw [← set_integral_condKernel hs MeasurableSet.univ hf]; simp_rw [Measure.restrict_univ] -#align probability_theory.set_integral_cond_kernel_univ_right ProbabilityTheory.set_integral_condKernel_univ_right - -theorem set_integral_condKernel_univ_left {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → E} - {t : Set Ω} (ht : MeasurableSet t) (hf : IntegrableOn f (univ ×ˢ t) ρ) : - ∫ a, ∫ ω in t, f (a, ω) ∂ρ.condKernel a ∂ρ.fst = ∫ x in univ ×ˢ t, f x ∂ρ := by - rw [← set_integral_condKernel MeasurableSet.univ ht hf]; simp_rw [Measure.restrict_univ] -#align probability_theory.set_integral_cond_kernel_univ_left ProbabilityTheory.set_integral_condKernel_univ_left - -end IntegralCondKernel - -section Unique - -/-! ### Uniqueness - -This section will prove that the conditional kernel is unique almost everywhere. -/ - -/-- A s-finite kernel which satisfy the disintegration property of the given measure `ρ` is almost -everywhere equal to the disintegration kernel of `ρ` when evaluated on a measurable set. - -This theorem in the case of finite kernels is weaker than `eq_condKernel_of_measure_eq_compProd` -which asserts that the kernels are equal almost everywhere and not just on a given measurable -set. -/ -theorem eq_condKernel_of_measure_eq_compProd' (κ : kernel α Ω) [IsSFiniteKernel κ] - (hκ : ρ = ρ.fst ⊗ₘ κ) {s : Set Ω} (hs : MeasurableSet s) : - ∀ᵐ x ∂ρ.fst, κ x s = ρ.condKernel x s := by - refine' ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite - (kernel.measurable_coe κ hs) (kernel.measurable_coe ρ.condKernel hs) _ - intros t ht _ - conv_rhs => rw [set_lintegral_condKernel_eq_measure_prod _ ht hs, hκ] - simp only [Measure.compProd_apply (ht.prod hs), Set.mem_prod, ← lintegral_indicator _ ht] - congr; ext x - by_cases hx : x ∈ t - all_goals simp [hx] - --- This lemma establishes uniqueness of the disintegration kernel on ℝ -lemma eq_condKernel_of_measure_eq_compProd_real (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] - (κ : kernel α ℝ) [IsFiniteKernel κ] (hκ : ρ = ρ.fst ⊗ₘ κ) : - ∀ᵐ x ∂ρ.fst, κ x = ρ.condKernel x := by - have huniv : ∀ᵐ x ∂ρ.fst, κ x Set.univ = ρ.condKernel x Set.univ := - eq_condKernel_of_measure_eq_compProd' ρ κ hκ MeasurableSet.univ - suffices ∀ᵐ x ∂ρ.fst, ∀ ⦃t⦄, MeasurableSet t → κ x t = ρ.condKernel x t by - filter_upwards [this] with x hx - ext t ht; exact hx ht - apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat - Real.isPiSystem_Iic_rat - · simp only [OuterMeasure.empty', Filter.eventually_true] - · simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff] - exact ae_all_iff.2 fun q => eq_condKernel_of_measure_eq_compProd' ρ κ hκ measurableSet_Iic - · filter_upwards [huniv] with x hxuniv t ht heq - rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _] - · filter_upwards with x f hdisj hf heq - rw [measure_iUnion hdisj hf, measure_iUnion hdisj hf] - exact tsum_congr heq - -/-- A finite kernel which satisfies the disintegration property is almost everywhere equal to the -disintegration kernel. -/ -theorem eq_condKernel_of_measure_eq_compProd (κ : kernel α Ω) [IsFiniteKernel κ] - (hκ : ρ = ρ.fst ⊗ₘ κ) : - ∀ᵐ x ∂ρ.fst, κ x = ρ.condKernel x := by --- The idea is to transporting the question to `ℝ` from `Ω` using `exists_measurableEmbedding_real` --- and then constructing a measure on `α × ℝ` using the obtained measurable embedding - obtain ⟨f, hf⟩ := exists_measurableEmbedding_real Ω - set ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f) with hρ'def - have hρ' : ρ'.fst = ρ.fst := by - ext s hs - rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_apply] - exacts [rfl, Measurable.prod measurable_fst <| hf.measurable.comp measurable_snd, - measurable_fst hs, hs, hs] - have hρ'' : ∀ᵐ x ∂ρ'.fst, kernel.map κ f hf.measurable x = ρ'.condKernel x := by - refine' eq_condKernel_of_measure_eq_compProd_real ρ' (kernel.map κ f hf.measurable) _ - ext s hs - simp only [ρ', Measure.map_apply (measurable_id.prod_map hf.measurable) hs] - conv_lhs => congr; rw [hκ] - rw [Measure.compProd_apply hs, Measure.compProd_apply - (measurable_id.prod_map hf.measurable hs), (_ : (ρ.map (Prod.map id f)).fst = ρ.fst)] - · congr - ext x - simp only [Set.mem_preimage, Prod_map, id_eq, kernel.prodMkLeft_apply, kernel.map_apply] - rw [Measure.map_apply hf.measurable] - · rfl - · exact measurable_prod_mk_left hs - · rw [Measure.fst_map_prod_mk] - · simp only [Prod_map, id_eq]; rfl - · exact (hf.measurable.comp measurable_snd) - rw [hρ'] at hρ'' - suffices ∀ᵐ x ∂ρ.fst, ∀ s, MeasurableSet s → - ((ρ.map (Prod.map id f)).condKernel x) s = (ρ.condKernel x) (f ⁻¹' s) by - filter_upwards [hρ'', this] with x hx h - rw [kernel.map_apply] at hx - ext s hs - rw [← Set.preimage_image_eq s hf.injective, - ← Measure.map_apply hf.measurable <| hf.measurableSet_image.2 hs, hx, - h _ <| hf.measurableSet_image.2 hs] - have hprod : (ρ.map (Prod.map id f)).fst = ρ.fst := by - ext s hs - rw [Measure.fst_apply hs, - Measure.map_apply (measurable_id.prod_map hf.measurable) (measurable_fst hs), - ← Set.preimage_comp, Measure.fst_apply hs] - rfl - suffices ρ.map (Prod.map id f) = - ((ρ.map (Prod.map id f)).fst ⊗ₘ (kernel.map (Measure.condKernel ρ) f hf.measurable)) by - have heq := eq_condKernel_of_measure_eq_compProd_real _ _ this - rw [hprod] at heq - filter_upwards [heq] with x hx s hs - rw [← hx, kernel.map_apply, Measure.map_apply hf.measurable hs] - ext s hs - simp only [hprod, Measure.compProd_apply hs, kernel.map_apply _ hf.measurable] - rw [Measure.map_apply (measurable_id.prod_map hf.measurable) hs, ← lintegral_condKernel_mem] - · simp only [mem_preimage, Prod_map, id_eq] - congr with a - rw [Measure.map_apply hf.measurable (measurable_prod_mk_left hs)] - rfl - · exact measurable_id.prod_map hf.measurable hs - -end Unique - -end StandardBorel - -end ProbabilityTheory - -namespace MeasureTheory - -/-! ### Integrability - -We place these lemmas in the `MeasureTheory` namespace to enable dot notation. -/ - - -open ProbabilityTheory - -variable {α Ω E F : Type*} {mα : MeasurableSpace α} [MeasurableSpace Ω] - [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] - [CompleteSpace E] [NormedAddCommGroup F] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] - -theorem AEStronglyMeasurable.ae_integrable_condKernel_iff {f : α × Ω → F} - (hf : AEStronglyMeasurable f ρ) : - (∀ᵐ a ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ - Integrable (fun a => ∫ ω, ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f ρ := by - rw [measure_eq_compProd ρ] at hf - conv_rhs => rw [measure_eq_compProd ρ] - rw [Measure.integrable_compProd_iff hf] -#align measure_theory.ae_strongly_measurable.ae_integrable_cond_kernel_iff MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff - -theorem Integrable.condKernel_ae {f : α × Ω → F} (hf_int : Integrable f ρ) : - ∀ᵐ a ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a) := by - have hf_ae : AEStronglyMeasurable f ρ := hf_int.1 - rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int - exact hf_int.1 -#align measure_theory.integrable.cond_kernel_ae MeasureTheory.Integrable.condKernel_ae - -theorem Integrable.integral_norm_condKernel {f : α × Ω → F} (hf_int : Integrable f ρ) : - Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst := by - have hf_ae : AEStronglyMeasurable f ρ := hf_int.1 - rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int - exact hf_int.2 -#align measure_theory.integrable.integral_norm_cond_kernel MeasureTheory.Integrable.integral_norm_condKernel - -theorem Integrable.norm_integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) : - Integrable (fun x => ‖∫ y, f (x, y) ∂ρ.condKernel x‖) ρ.fst := by - refine' hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm _ - filter_upwards with x - rw [norm_norm] - refine' (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg _).symm - exact integral_nonneg_of_ae (eventually_of_forall fun y => norm_nonneg _) -#align measure_theory.integrable.norm_integral_cond_kernel MeasureTheory.Integrable.norm_integral_condKernel - -theorem Integrable.integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) : - Integrable (fun x => ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst := - (integrable_norm_iff hf_int.1.integral_condKernel).mp hf_int.norm_integral_condKernel -#align measure_theory.integrable.integral_cond_kernel MeasureTheory.Integrable.integral_condKernel - -end MeasureTheory diff --git a/Mathlib/Probability/Kernel/Disintegration/Basic.lean b/Mathlib/Probability/Kernel/Disintegration/Basic.lean new file mode 100644 index 0000000000000..4d56a6bd7318f --- /dev/null +++ b/Mathlib/Probability/Kernel/Disintegration/Basic.lean @@ -0,0 +1,525 @@ +/- +Copyright (c) 2024 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.MeasureCompProd +import Mathlib.Probability.Kernel.Disintegration.CondCdf +import Mathlib.Probability.Kernel.Disintegration.Density +import Mathlib.Probability.Kernel.Disintegration.CdfToKernel + +/-! +# Disintegration of kernels and measures + +Let `κ : kernel α (β × Ω)` be a finite kernel, where `Ω` is a standard Borel space. Then if `α` is +countable or `β` has a countably generated σ-algebra (for example if it is standard Borel), then +there exists a `kernel (α × β) Ω` called conditional kernel and denoted by `condKernel κ` such that +`κ = fst κ ⊗ₖ condKernel κ`. +We also define a conditional kernel for a measure `ρ : Measure (β × Ω)`, where `Ω` is a standard +Borel space. This is a `kernel β Ω` denoted by `ρ.condKernel` such that `ρ = ρ.fst ⊗ₘ ρ.condKernel`. + +In order to obtain a disintegration for any standard Borel space `Ω`, we use that these spaces embed +measurably into `ℝ`: it then suffices to define a suitable kernel for `Ω = ℝ`. + +For `κ : kernel α (β × ℝ)`, the construction of the conditional kernel proceeds as follows: +* Build a measurable function `f : (α × β) → ℚ → ℝ` such that for all measurable sets + `s` and all `q : ℚ`, `∫ x in s, f (a, x) q ∂(kernel.fst κ a) = (κ a (s ×ˢ Iic (q : ℝ))).toReal`. + We restrict to `ℚ` here to be able to prove the measurability. +* Extend that function to `(α × β) → StieltjesFunction`. See the file `MeasurableStieltjes.lean`. +* Finally obtain from the measurable Stieltjes function a measure on `ℝ` for each element of `α × β` + in a measurable way: we have obtained a `kernel (α × β) ℝ`. + See the file `CdfToKernel.lean` for that step. + +The first step (building the measurable function on `ℚ`) is done differently depending on whether +`α` is countable or not. +* If `α` is countable, we can provide for each `a : α` a function `f : β → ℚ → ℝ` and proceed as + above to obtain a `kernel β ℝ`. Since `α` is countable, measurability is not an issue and we can + put those together into a `kernel (α × β) ℝ`. The construction of that `f` is done in + the `CondCdf.lean` file. +* If `α` is not countable, we can't proceed separately for each `a : α` and have to build a function + `f : α × β → ℚ → ℝ` which is measurable on the product. We are able to do so if `β` has a + countably generated σ-algebra (this is the case in particular for standard Borel spaces). + See the file `Density.lean`. + +The conditional kernel is defined under the typeclass assumption +`CountableOrCountablyGenerated α β`, which encodes the property +`Countable α ∨ CountablyGenerated β`. + +Properties of integrals involving `condKernel` are collated in the file `Integral.lean`. +The conditional kernel is unique (almost everywhere w.r.t. `fst κ`): this is proved in the file +`Unique.lean`. + +## Main definitions + +* `ProbabilityTheory.kernel.condKernel κ : kernel (α × β) Ω`: conditional kernel described above. +* `MeasureTheory.Measure.condKernel ρ : kernel β Ω`: conditional kernel of a measure. + +## Main statements + +* `ProbabilityTheory.kernel.compProd_fst_condKernel`: `fst κ ⊗ₖ condKernel κ = κ` +* `MeasureTheory.Measure.compProd_fst_condKernel`: `ρ.fst ⊗ₘ ρ.condKernel = ρ` +-/ + +#align_import probability.kernel.disintegration from "leanprover-community/mathlib"@"6315581f5650ffa2fbdbbbedc41243c8d7070981" + +open MeasureTheory Set Filter MeasurableSpace + +open scoped ENNReal MeasureTheory Topology ProbabilityTheory + +#noalign probability_theory.cond_kernel_real +#noalign probability_theory.cond_kernel_real_Iic +#noalign probability_theory.set_lintegral_cond_kernel_real_Iic +#noalign probability_theory.set_lintegral_cond_kernel_real_univ +#noalign probability_theory.lintegral_cond_kernel_real_univ +#noalign probability_theory.set_lintegral_cond_kernel_real_prod +#noalign probability_theory.lintegral_cond_kernel_real_mem +#noalign probability_theory.kernel.const_eq_comp_prod_real +#noalign probability_theory.measure_eq_comp_prod_real +#noalign probability_theory.lintegral_cond_kernel_real +#noalign probability_theory.ae_cond_kernel_real_eq_one +#noalign probability_theory.exists_cond_kernel +#noalign probability_theory.cond_kernel_def +#noalign probability_theory.kernel.const_unit_eq_comp_prod +#noalign probability_theory.kernel.const_eq_comp_prod + +namespace ProbabilityTheory.kernel + +variable {α β γ Ω : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] + [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + +section Real + +/-! ### Disintegration of kernels from `α` to `γ × ℝ` for countably generated `γ` -/ + +lemma isRatCondKernelCDFAux_density_Iic (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : + IsRatCondKernelCDFAux (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ) + where + measurable := measurable_pi_iff.mpr fun _ ↦ measurable_density κ (fst κ) measurableSet_Iic + mono' a q r hqr := + ae_of_all _ fun c ↦ density_mono_set le_rfl a c (Iic_subset_Iic.mpr (by exact_mod_cast hqr)) + nonneg' a q := ae_of_all _ fun c ↦ density_nonneg le_rfl _ _ _ + le_one' a q := ae_of_all _ fun c ↦ density_le_one le_rfl _ _ _ + tendsto_integral_of_antitone a s hs_anti hs_tendsto := by + let s' : ℕ → Set ℝ := fun n ↦ Iic (s n) + refine tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic) + · refine fun i j hij ↦ Iic_subset_Iic.mpr ?_ + exact mod_cast hs_anti hij + · ext x + simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false, not_forall, not_le, s'] + rw [tendsto_atTop_atBot] at hs_tendsto + have ⟨q, hq⟩ := exists_rat_lt x + obtain ⟨i, hi⟩ := hs_tendsto q + refine ⟨i, lt_of_le_of_lt ?_ hq⟩ + exact mod_cast hi i le_rfl + tendsto_integral_of_monotone a s hs_mono hs_tendsto := by + rw [fst_apply' _ _ MeasurableSet.univ] + let s' : ℕ → Set ℝ := fun n ↦ Iic (s n) + refine tendsto_integral_density_of_monotone (le_rfl : fst κ ≤ fst κ) + a s' ?_ ?_ (fun _ ↦ measurableSet_Iic) + · exact fun i j hij ↦ Iic_subset_Iic.mpr (by exact mod_cast hs_mono hij) + · ext x + simp only [mem_iUnion, mem_Iic, mem_univ, iff_true] + rw [tendsto_atTop_atTop] at hs_tendsto + have ⟨q, hq⟩ := exists_rat_gt x + obtain ⟨i, hi⟩ := hs_tendsto q + refine ⟨i, hq.le.trans ?_⟩ + exact mod_cast hi i le_rfl + integrable a q := integrable_density le_rfl a measurableSet_Iic + set_integral a A hA q := set_integral_density le_rfl a measurableSet_Iic hA + +/-- Taking the kernel density of intervals `Iic q` for `q : ℚ` gives a function with the property +`isRatCondKernelCDF`. -/ +lemma isRatCondKernelCDF_density_Iic (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : + IsRatCondKernelCDF (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ) := + (isRatCondKernelCDFAux_density_Iic κ).isRatCondKernelCDF + +/-- The conditional kernel CDF of a kernel `κ : kernel α (γ × ℝ)`, where `γ` is countably generated. +-/ +noncomputable +def condKernelCDF (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : α × γ → StieltjesFunction := + stieltjesOfMeasurableRat (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) + (isRatCondKernelCDF_density_Iic κ).measurable + +lemma isCondKernelCDF_condKernelCDF (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : + IsCondKernelCDF (condKernelCDF κ) κ (fst κ) := + isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_density_Iic κ) + +/-- Auxiliary definition for `ProbabilityTheory.kernel.condKernel`. +A conditional kernel for `κ : kernel α (γ × ℝ)` where `γ` is countably generated. -/ +noncomputable +def condKernelReal (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : kernel (α × γ) ℝ := + (isCondKernelCDF_condKernelCDF κ).toKernel + +instance instIsMarkovKernelCondKernelReal (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : + IsMarkovKernel (condKernelReal κ) := by + rw [condKernelReal] + infer_instance + +lemma compProd_fst_condKernelReal (κ : kernel α (γ × ℝ)) [IsFiniteKernel κ] : + fst κ ⊗ₖ condKernelReal κ = κ := by + rw [condKernelReal, compProd_toKernel] + +/-- Auxiliary definition for `MeasureTheory.Measure.condKernel` and +`ProbabilityTheory.kernel.condKernel`. +A conditional kernel for `κ : kernel Unit (α × ℝ)`. -/ +noncomputable +def condKernelUnitReal (κ : kernel Unit (α × ℝ)) [IsFiniteKernel κ] : kernel (Unit × α) ℝ := + (isCondKernelCDF_condCDF (κ ())).toKernel + +instance instIsMarkovKernelCondKernelUnitReal (κ : kernel Unit (α × ℝ)) [IsFiniteKernel κ] : + IsMarkovKernel (condKernelUnitReal κ) := by + rw [condKernelUnitReal] + infer_instance + +lemma compProd_fst_condKernelUnitReal (κ : kernel Unit (α × ℝ)) [IsFiniteKernel κ] : + fst κ ⊗ₖ condKernelUnitReal κ = κ := by + rw [condKernelUnitReal, compProd_toKernel] + ext a + simp + +end Real + +section BorelSnd + +/-! ### Disintegration of kernels on standard Borel spaces + +Since every standard Borel space embeds measurably into `ℝ`, we can generalize a disintegration +property on `ℝ` to all these spaces. -/ + +open Classical in +/-- Auxiliary definition for `ProbabilityTheory.kernel.condKernel`. +A Borel space `Ω` embeds measurably into `ℝ` (with embedding `e`), hence we can get a `kernel α Ω` +from a `kernel α ℝ` by taking the comap by `e`. +Here we take the comap of a modification of `η : kernel α ℝ`, useful when `η a` is a probability +measure with all its mass on `range e` almost everywhere with respect to some measure and we want to +ensure that the comap is a Markov kernel. +We thus take the comap by `e` of a kernel defined piecewise: `η` when +`η a (range (embeddingReal Ω))ᶜ = 0`, and an arbitrary deterministic kernel otherwise. -/ +noncomputable +def borelMarkovFromReal (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] + (η : kernel α ℝ) : + kernel α Ω := + have he := measurableEmbedding_embeddingReal Ω + let x₀ := (range_nonempty (embeddingReal Ω)).choose + comapRight + (piecewise ((kernel.measurable_coe η he.measurableSet_range.compl) (measurableSet_singleton 0) : + MeasurableSet {a | η a (range (embeddingReal Ω))ᶜ = 0}) + η (deterministic (fun _ ↦ x₀) measurable_const)) he + +lemma borelMarkovFromReal_apply (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] + (η : kernel α ℝ) (a : α) : + borelMarkovFromReal Ω η a + = if η a (range (embeddingReal Ω))ᶜ = 0 then (η a).comap (embeddingReal Ω) + else (Measure.dirac (range_nonempty (embeddingReal Ω)).choose).comap (embeddingReal Ω) := by + classical + rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply] + simp only [mem_preimage, mem_singleton_iff] + split_ifs <;> rfl + +lemma borelMarkovFromReal_apply' (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] + (η : kernel α ℝ) (a : α) {s : Set Ω} (hs : MeasurableSet s) : + borelMarkovFromReal Ω η a s + = if η a (range (embeddingReal Ω))ᶜ = 0 then η a (embeddingReal Ω '' s) + else (embeddingReal Ω '' s).indicator 1 (range_nonempty (embeddingReal Ω)).choose := by + have he := measurableEmbedding_embeddingReal Ω + rw [borelMarkovFromReal_apply] + split_ifs with h + · rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs] + · rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply] + +/-- When `η` is an s-finite kernel, `borelMarkovFromReal Ω η` is an s-finite kernel. -/ +instance instIsSFiniteKernelBorelMarkovFromReal (η : kernel α ℝ) [IsSFiniteKernel η] : + IsSFiniteKernel (borelMarkovFromReal Ω η) := + IsSFiniteKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) + +/-- When `η` is a finite kernel, `borelMarkovFromReal Ω η` is a finite kernel. -/ +instance instIsFiniteKernelBorelMarkovFromReal (η : kernel α ℝ) [IsFiniteKernel η] : + IsFiniteKernel (borelMarkovFromReal Ω η) := + IsFiniteKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) + +/-- When `η` is a Markov kernel, `borelMarkovFromReal Ω η` is a Markov kernel. -/ +instance instIsMarkovKernelBorelMarkovFromReal (η : kernel α ℝ) [IsMarkovKernel η] : + IsMarkovKernel (borelMarkovFromReal Ω η) := by + refine IsMarkovKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) (fun a ↦ ?_) + classical + rw [piecewise_apply] + split_ifs with h + · rwa [← prob_compl_eq_zero_iff (measurableEmbedding_embeddingReal Ω).measurableSet_range] + · rw [deterministic_apply] + simp [(range_nonempty (embeddingReal Ω)).choose_spec] + +/-- For `κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable)`, the +hypothesis `hη` is `fst κ' ⊗ₖ η = κ'`. The conclusion of the lemma is +`fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) _`. -/ +lemma compProd_fst_borelMarkovFromReal_eq_comapRight_compProd + (κ : kernel α (β × Ω)) [IsSFiniteKernel κ] (η : kernel (α × β) ℝ) [IsSFiniteKernel η] + (hη : (fst (map κ (Prod.map (id : β → β) (embeddingReal Ω)) + (measurable_id.prod_map (measurableEmbedding_embeddingReal Ω).measurable))) ⊗ₖ η + = map κ (Prod.map (id : β → β) (embeddingReal Ω)) + (measurable_id.prod_map (measurableEmbedding_embeddingReal Ω).measurable)) : + fst κ ⊗ₖ borelMarkovFromReal Ω η + = comapRight (fst (map κ (Prod.map (id : β → β) (embeddingReal Ω)) + (measurable_id.prod_map (measurableEmbedding_embeddingReal Ω).measurable)) ⊗ₖ η) + (MeasurableEmbedding.id.prod_mk (measurableEmbedding_embeddingReal Ω)) := by + let e := embeddingReal Ω + let he := measurableEmbedding_embeddingReal Ω + let κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable) + have hη' : fst κ' ⊗ₖ η = κ' := hη + have h_prod_embed : MeasurableEmbedding (Prod.map (id : β → β) e) := + MeasurableEmbedding.id.prod_mk he + change fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) h_prod_embed + rw [comapRight_compProd_id_prod _ _ he] + have h_fst : fst κ' = fst κ := by + ext a u + unfold_let κ' + rw [fst_apply, map_apply, Measure.map_map measurable_fst h_prod_embed.measurable, fst_apply] + congr + rw [h_fst] + ext a t ht : 2 + simp_rw [compProd_apply _ _ _ ht] + refine lintegral_congr_ae ?_ + have h_ae : ∀ᵐ t ∂(fst κ a), (a, t) ∈ {p : α × β | η p (range e)ᶜ = 0} := by + rw [← h_fst] + have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by + unfold_let κ' + rw [map_apply'] + swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl + suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp + ext x + simp + rw [← hη', compProd_null] at h_compProd + swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl + simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd + exact h_compProd + filter_upwards [h_ae] with a ha + rw [borelMarkovFromReal, comapRight_apply', comapRight_apply'] + rotate_left + · exact measurable_prod_mk_left ht + · exact measurable_prod_mk_left ht + classical + rw [piecewise_apply, if_pos] + exact ha + +/-- For `κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable)`, the +hypothesis `hη` is `fst κ' ⊗ₖ η = κ'`. With that hypothesis, +`fst κ ⊗ₖ borelMarkovFromReal κ η = κ`.-/ +lemma compProd_fst_borelMarkovFromReal (κ : kernel α (β × Ω)) [IsSFiniteKernel κ] + (η : kernel (α × β) ℝ) [IsSFiniteKernel η] + (hη : (fst (map κ (Prod.map (id : β → β) (embeddingReal Ω)) + (measurable_id.prod_map (measurableEmbedding_embeddingReal Ω).measurable))) ⊗ₖ η + = map κ (Prod.map (id : β → β) (embeddingReal Ω)) + (measurable_id.prod_map (measurableEmbedding_embeddingReal Ω).measurable)) : + fst κ ⊗ₖ borelMarkovFromReal Ω η = κ := by + let e := embeddingReal Ω + let he := measurableEmbedding_embeddingReal Ω + let κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable) + have hη' : fst κ' ⊗ₖ η = κ' := hη + have h_prod_embed : MeasurableEmbedding (Prod.map (id : β → β) e) := + MeasurableEmbedding.id.prod_mk he + have : κ = comapRight κ' h_prod_embed := by + ext c t : 2 + unfold_let κ' + rw [comapRight_apply, map_apply, h_prod_embed.comap_map] + conv_rhs => rw [this, ← hη'] + exact compProd_fst_borelMarkovFromReal_eq_comapRight_compProd κ η hη + +end BorelSnd + +section CountablyGenerated + +open ProbabilityTheory.kernel + +/-- Auxiliary definition for `ProbabilityTheory.kernel.condKernel`. +A conditional kernel for `κ : kernel α (γ × Ω)` where `γ` is countably generated and `Ω` is +standard Borel. -/ +noncomputable +def condKernelBorel (κ : kernel α (γ × Ω)) [IsFiniteKernel κ] : kernel (α × γ) Ω := + let e := embeddingReal Ω + let he := measurableEmbedding_embeddingReal Ω + let κ' := map κ (Prod.map (id : γ → γ) e) (measurable_id.prod_map he.measurable) + borelMarkovFromReal Ω (condKernelReal κ') + +instance instIsMarkovKernelCondKernelBorel (κ : kernel α (γ × Ω)) [IsFiniteKernel κ] : + IsMarkovKernel (condKernelBorel κ) := by + rw [condKernelBorel] + infer_instance + +lemma compProd_fst_condKernelBorel (κ : kernel α (γ × Ω)) [IsFiniteKernel κ] : + fst κ ⊗ₖ condKernelBorel κ = κ := by + rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)] + +end CountablyGenerated + +section Unit + +/-- Auxiliary definition for `MeasureTheory.Measure.condKernel` and +`ProbabilityTheory.kernel.condKernel`. +A conditional kernel for `κ : kernel Unit (α × Ω)` where `Ω` is standard Borel. -/ +noncomputable +def condKernelUnitBorel (κ : kernel Unit (α × Ω)) [IsFiniteKernel κ] : kernel (Unit × α) Ω := + let e := embeddingReal Ω + let he := measurableEmbedding_embeddingReal Ω + let κ' := map κ (Prod.map (id : α → α) e) (measurable_id.prod_map he.measurable) + borelMarkovFromReal Ω (condKernelUnitReal κ') + +instance instIsMarkovKernelCondKernelUnitBorel (κ : kernel Unit (α × Ω)) [IsFiniteKernel κ] : + IsMarkovKernel (condKernelUnitBorel κ) := by + rw [condKernelUnitBorel] + infer_instance + +lemma compProd_fst_condKernelUnitBorel (κ : kernel Unit (α × Ω)) [IsFiniteKernel κ] : + fst κ ⊗ₖ condKernelUnitBorel κ = κ := by + rw [condKernelUnitBorel, + compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelUnitReal _)] + +end Unit + +section Measure + +variable {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] + +/-- Conditional kernel of a measure on a product space: a Markov kernel such that +`ρ = ρ.fst ⊗ₘ ρ.condKernel` (see `MeasureTheory.Measure.compProd_fst_condKernel`). -/ +noncomputable +irreducible_def _root_.MeasureTheory.Measure.condKernel (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : + kernel α Ω := + comap (condKernelUnitBorel (const Unit ρ)) (fun a ↦ ((), a)) measurable_prod_mk_left +#align measure_theory.measure.cond_kernel MeasureTheory.Measure.condKernel + +lemma _root_.MeasureTheory.Measure.condKernel_apply (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] + (a : α) : + ρ.condKernel a = condKernelUnitBorel (const Unit ρ) ((), a) := by + rw [Measure.condKernel]; rfl + +instance _root_.MeasureTheory.Measure.instIsMarkovKernelCondKernel + (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : IsMarkovKernel ρ.condKernel := by + rw [Measure.condKernel] + infer_instance + +/-- **Disintegration** of finite product measures on `α × Ω`, where `Ω` is standard Borel. Such a +measure can be written as the composition-product of `ρ.fst` (marginal measure over `α`) and +a Markov kernel from `α` to `Ω`. We call that Markov kernel `ρ.condKernel`. -/ +lemma _root_.MeasureTheory.Measure.compProd_fst_condKernel + (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : + ρ.fst ⊗ₘ ρ.condKernel = ρ := by + have h1 : const Unit (Measure.fst ρ) = fst (const Unit ρ) := by + ext + simp only [fst_apply, Measure.fst, const_apply] + have h2 : prodMkLeft Unit (Measure.condKernel ρ) = condKernelUnitBorel (const Unit ρ) := by + ext + simp only [prodMkLeft_apply, Measure.condKernel_apply] + rw [Measure.compProd, h1, h2, compProd_fst_condKernelUnitBorel] + simp +#align probability_theory.measure_eq_comp_prod MeasureTheory.Measure.compProd_fst_condKernel + +/-- Auxiliary lemma for `condKernel_apply_of_ne_zero`. -/ +lemma _root_.MeasureTheory.Measure.condKernel_apply_of_ne_zero_of_measurableSet + [MeasurableSingletonClass α] {x : α} (hx : ρ.fst {x} ≠ 0) {s : Set Ω} (hs : MeasurableSet s) : + ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) := by + nth_rewrite 3 [← ρ.compProd_fst_condKernel] + rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))] + classical + have : ∀ a, ρ.condKernel a (Prod.mk a ⁻¹' {x} ×ˢ s) + = ({x} : Set α).indicator (fun a ↦ ρ.condKernel a s) a := by + intro a + by_cases hax : a = x + · simp only [hax, singleton_prod, mem_singleton_iff, indicator_of_mem] + congr with y + simp + · simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_not_mem] + have : Prod.mk a ⁻¹' (Prod.mk x '' s) = ∅ := by + ext y + simp [Ne.symm hax] + simp only [this, measure_empty] + simp_rw [this] + rw [MeasureTheory.lintegral_indicator _ (measurableSet_singleton x)] + simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac] + rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top ρ.fst _), one_mul] + +/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`, +`ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` . -/ +lemma _root_.MeasureTheory.Measure.condKernel_apply_of_ne_zero [MeasurableSingletonClass α] + {x : α} (hx : ρ.fst {x} ≠ 0) (s : Set Ω) : + ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) := by + have : ρ.condKernel x s = ((ρ.fst {x})⁻¹ • ρ).comap (fun (y : Ω) ↦ (x, y)) s := by + congr 2 with s hs + simp [Measure.condKernel_apply_of_ne_zero_of_measurableSet hx hs, + (measurableEmbedding_prod_mk_left x).comap_apply] + simp [this, (measurableEmbedding_prod_mk_left x).comap_apply, hx] + +end Measure + +section Countable + +variable [Countable α] + +/-- Auxiliary definition for `ProbabilityTheory.kernel.condKernel`. +A conditional kernel for `κ : kernel α (β × Ω)` where `α` is countable and `Ω` is standard Borel. -/ +noncomputable +def condKernelCountable (κ : kernel α (β × Ω)) [IsFiniteKernel κ] : kernel (α × β) Ω where + val p := (κ p.1).condKernel p.2 + property := by + change Measurable ((fun q : β × α ↦ (κ q.2).condKernel q.1) ∘ Prod.swap) + refine (measurable_from_prod_countable' (fun a ↦ ?_) ?_).comp measurable_swap + · exact kernel.measurable (κ a).condKernel + · intro y y' x hy' + have : κ y' = κ y := by + ext s hs + exact mem_of_mem_measurableAtom hy' + (kernel.measurable_coe κ hs (measurableSet_singleton (κ y s))) rfl + simp [this] + +lemma condKernelCountable_apply (κ : kernel α (β × Ω)) [IsFiniteKernel κ] (p : α × β) : + condKernelCountable κ p = (κ p.1).condKernel p.2 := rfl + +instance instIsMarkovKernelCondKernelCountable (κ : kernel α (β × Ω)) [IsFiniteKernel κ] : + IsMarkovKernel (condKernelCountable κ) := + ⟨fun p ↦ (Measure.instIsMarkovKernelCondKernel (κ p.1)).isProbabilityMeasure p.2⟩ + +lemma compProd_fst_condKernelCountable (κ : kernel α (β × Ω)) [IsFiniteKernel κ] : + fst κ ⊗ₖ condKernelCountable κ = κ := by + ext a s hs + have h := (κ a).compProd_fst_condKernel + conv_rhs => rw [← h] + simp_rw [compProd_apply _ _ _ hs, condKernelCountable_apply, Measure.compProd_apply hs] + congr + +end Countable + +section CountableOrCountablyGenerated + +open Classical in + +/-- Conditional kernel of a kernel `κ : kernel α (β × Ω)`: a Markov kernel such that +`fst κ ⊗ₖ condKernel κ = κ` (see `MeasureTheory.Measure.compProd_fst_condKernel`). +It exists whenever `Ω` is standard Borel and either `α` is countable +or `β` is countably generated. -/ +noncomputable +irreducible_def condKernel [h : CountableOrCountablyGenerated α β] + (κ : kernel α (β × Ω)) [IsFiniteKernel κ] : + kernel (α × β) Ω := + if hα : Countable α then condKernelCountable κ + else letI := h.countableOrCountablyGenerated.resolve_left hα; condKernelBorel κ + +/-- `condKernel κ` is a Markov kernel. -/ +instance instIsMarkovKernelCondKernel [CountableOrCountablyGenerated α β] + (κ : kernel α (β × Ω)) [IsFiniteKernel κ] : + IsMarkovKernel (condKernel κ) := by + rw [condKernel_def] + split_ifs <;> infer_instance + +/-- **Disintegration** of finite kernels. +The composition-product of `fst κ` and `condKernel κ` is equal to `κ`. -/ +lemma compProd_fst_condKernel [hαβ : CountableOrCountablyGenerated α β] + (κ : kernel α (β × Ω)) [IsFiniteKernel κ] : + fst κ ⊗ₖ condKernel κ = κ := by + rw [condKernel_def] + split_ifs with h + · exact compProd_fst_condKernelCountable κ + · have := hαβ.countableOrCountablyGenerated.resolve_left h + exact compProd_fst_condKernelBorel κ + +end CountableOrCountablyGenerated + +end ProbabilityTheory.kernel diff --git a/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean b/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean index 0a0f49623bc3a..265c92f387fd4 100644 --- a/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean +++ b/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean @@ -657,27 +657,6 @@ lemma compProd_toKernel [IsFiniteKernel κ] [IsSFiniteKernel ν] (hf : IsCondKer ext a s hs rw [kernel.compProd_apply _ _ _ hs, lintegral_toKernel_mem hf a hs] -lemma ae_toKernel_eq_one [IsFiniteKernel κ] [IsSFiniteKernel ν] (hf : IsCondKernelCDF f κ ν) (a : α) - {s : Set ℝ} (hs : MeasurableSet s) (hκs : κ a {x | x.snd ∈ sᶜ} = 0) : - ∀ᵐ b ∂(ν a), hf.toKernel f (a, b) s = 1 := by - have h_eq : ν ⊗ₖ hf.toKernel f = κ := compProd_toKernel hf - have h : κ a {x | x.snd ∈ sᶜ} = (ν ⊗ₖ hf.toKernel f) a {x | x.snd ∈ sᶜ} := by rw [h_eq] - rw [hκs, kernel.compProd_apply] at h - swap; · exact measurable_snd hs.compl - rw [eq_comm, lintegral_eq_zero_iff] at h - swap - · simp only [mem_compl_iff, mem_setOf_eq] - change Measurable ((fun p ↦ hf.toKernel f p {c | c ∉ s}) ∘ (fun b : β ↦ (a, b))) - exact (kernel.measurable_coe _ hs.compl).comp measurable_prod_mk_left - simp only [mem_compl_iff, mem_setOf_eq, kernel.prodMkLeft_apply'] at h - filter_upwards [h] with b hb - rwa [← compl_def, Pi.zero_apply, prob_compl_eq_zero_iff hs] at hb - -lemma measurableSet_toKernel_eq_one (hf : IsCondKernelCDF f κ ν) - {s : Set ℝ} (hs : MeasurableSet s) : - MeasurableSet {p | hf.toKernel f p s = 1} := - (kernel.measurable_coe _ hs) (measurableSet_singleton 1) - end end ProbabilityTheory diff --git a/Mathlib/Probability/Kernel/Disintegration/Integral.lean b/Mathlib/Probability/Kernel/Disintegration/Integral.lean new file mode 100644 index 0000000000000..02aa9b7301509 --- /dev/null +++ b/Mathlib/Probability/Kernel/Disintegration/Integral.lean @@ -0,0 +1,280 @@ +/- +Copyright (c) 2024 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.Basic + +/-! +# Lebesgue and Bochner integrals of conditional kernels + +Integrals of `ProbabilityTheory.kernel.condKernel` and `MeasureTheory.Measure.condKernel`. + +## Main statements + +* `ProbabilityTheory.set_integral_condKernel`: the integral + `∫ b in s, ∫ ω in t, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a)` is equal to + `∫ x in s ×ˢ t, f x ∂(κ a)`. +* `MeasureTheory.Measure.set_integral_condKernel`: + `∫ b in s, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ` + +Corresponding statements for the Lebesgue integral and/or without the sets `s` and `t` are also +provided. +-/ + +open MeasureTheory ProbabilityTheory MeasurableSpace + +open scoped ENNReal + +namespace ProbabilityTheory + +variable {α β Ω : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + +section Lintegral + +variable [CountableOrCountablyGenerated α β] {κ : kernel α (β × Ω)} [IsFiniteKernel κ] + {f : β × Ω → ℝ≥0∞} + +lemma lintegral_condKernel_mem (a : α) {s : Set (β × Ω)} (hs : MeasurableSet s) : + ∫⁻ x, kernel.condKernel κ (a, x) {y | (x, y) ∈ s} ∂(kernel.fst κ a) = κ a s := by + conv_rhs => rw [← kernel.compProd_fst_condKernel κ] + simp_rw [kernel.compProd_apply _ _ _ hs] + +lemma set_lintegral_condKernel_eq_measure_prod (a : α) {s : Set β} (hs : MeasurableSet s) + {t : Set Ω} (ht : MeasurableSet t) : + ∫⁻ b in s, kernel.condKernel κ (a, b) t ∂(kernel.fst κ a) = κ a (s ×ˢ t) := by + have : κ a (s ×ˢ t) = (kernel.fst κ ⊗ₖ kernel.condKernel κ) a (s ×ˢ t) := by + congr; exact (kernel.compProd_fst_condKernel κ).symm + rw [this, kernel.compProd_apply _ _ _ (hs.prod ht)] + classical + have : ∀ b, kernel.condKernel κ (a, b) {c | (b, c) ∈ s ×ˢ t} + = s.indicator (fun b ↦ kernel.condKernel κ (a, b) t) b := by + intro b + by_cases hb : b ∈ s <;> simp [hb] + simp_rw [this] + rw [lintegral_indicator _ hs] + +lemma lintegral_condKernel (hf : Measurable f) (a : α) : + ∫⁻ b, ∫⁻ ω, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) = ∫⁻ x, f x ∂(κ a) := by + conv_rhs => rw [← kernel.compProd_fst_condKernel κ] + rw [kernel.lintegral_compProd _ _ _ hf] + +lemma set_lintegral_condKernel (hf : Measurable f) (a : α) {s : Set β} + (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : + ∫⁻ b in s, ∫⁻ ω in t, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) + = ∫⁻ x in s ×ˢ t, f x ∂(κ a) := by + conv_rhs => rw [← kernel.compProd_fst_condKernel κ] + rw [kernel.set_lintegral_compProd _ _ _ hf hs ht] + +lemma set_lintegral_condKernel_univ_right (hf : Measurable f) (a : α) {s : Set β} + (hs : MeasurableSet s) : + ∫⁻ b in s, ∫⁻ ω, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) + = ∫⁻ x in s ×ˢ Set.univ, f x ∂(κ a) := by + rw [← set_lintegral_condKernel hf a hs MeasurableSet.univ]; simp_rw [Measure.restrict_univ] + +lemma set_lintegral_condKernel_univ_left (hf : Measurable f) (a : α) {t : Set Ω} + (ht : MeasurableSet t) : + ∫⁻ b, ∫⁻ ω in t, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) + = ∫⁻ x in Set.univ ×ˢ t, f x ∂(κ a) := by + rw [← set_lintegral_condKernel hf a MeasurableSet.univ ht]; simp_rw [Measure.restrict_univ] + +end Lintegral + +section Integral + +variable [CountableOrCountablyGenerated α β] {κ : kernel α (β × Ω)} [IsFiniteKernel κ] + {E : Type*} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] + +lemma _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel (a : α) + (hf : AEStronglyMeasurable f (κ a)) : + AEStronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂(kernel.condKernel κ (a, x))) + (kernel.fst κ a) := by + rw [← kernel.compProd_fst_condKernel κ] at hf + exact AEStronglyMeasurable.integral_kernel_compProd hf + +lemma integral_condKernel (a : α) (hf : Integrable f (κ a)) : + ∫ b, ∫ ω, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) = ∫ x, f x ∂(κ a) := by + conv_rhs => rw [← kernel.compProd_fst_condKernel κ] + rw [← kernel.compProd_fst_condKernel κ] at hf + rw [integral_compProd hf] + +lemma set_integral_condKernel (a : α) {s : Set β} (hs : MeasurableSet s) + {t : Set Ω} (ht : MeasurableSet t) (hf : IntegrableOn f (s ×ˢ t) (κ a)) : + ∫ b in s, ∫ ω in t, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) + = ∫ x in s ×ˢ t, f x ∂(κ a) := by + conv_rhs => rw [← kernel.compProd_fst_condKernel κ] + rw [← kernel.compProd_fst_condKernel κ] at hf + rw [set_integral_compProd hs ht hf] + +lemma set_integral_condKernel_univ_right (a : α) {s : Set β} (hs : MeasurableSet s) + (hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)) : + ∫ b in s, ∫ ω, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) + = ∫ x in s ×ˢ Set.univ, f x ∂(κ a) := by + rw [← set_integral_condKernel a hs MeasurableSet.univ hf]; simp_rw [Measure.restrict_univ] + +lemma set_integral_condKernel_univ_left (a : α) {t : Set Ω} (ht : MeasurableSet t) + (hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)) : + ∫ b, ∫ ω in t, f (b, ω) ∂(kernel.condKernel κ (a, b)) ∂(kernel.fst κ a) + = ∫ x in Set.univ ×ˢ t, f x ∂(κ a) := by + rw [← set_integral_condKernel a MeasurableSet.univ ht hf]; simp_rw [Measure.restrict_univ] + +end Integral + +end ProbabilityTheory + +namespace MeasureTheory.Measure + +variable {α β Ω : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + +section Lintegral + +variable [CountableOrCountablyGenerated α β] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] + {f : β × Ω → ℝ≥0∞} + +lemma lintegral_condKernel_mem {s : Set (β × Ω)} (hs : MeasurableSet s) : + ∫⁻ x, ρ.condKernel x {y | (x, y) ∈ s} ∂ρ.fst = ρ s := by + conv_rhs => rw [← compProd_fst_condKernel ρ] + simp_rw [compProd_apply hs] + rfl +#align probability_theory.lintegral_cond_kernel_mem MeasureTheory.Measure.lintegral_condKernel_mem + +lemma set_lintegral_condKernel_eq_measure_prod {s : Set β} (hs : MeasurableSet s) {t : Set Ω} + (ht : MeasurableSet t) : + ∫⁻ b in s, ρ.condKernel b t ∂ρ.fst = ρ (s ×ˢ t) := by + have : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t) := by + congr; exact (compProd_fst_condKernel ρ).symm + rw [this, compProd_apply (hs.prod ht)] + classical + have : ∀ b, ρ.condKernel b (Prod.mk b ⁻¹' s ×ˢ t) + = s.indicator (fun b ↦ ρ.condKernel b t) b := by + intro b + by_cases hb : b ∈ s <;> simp [hb] + simp_rw [this] + rw [lintegral_indicator _ hs] +#align probability_theory.set_lintegral_cond_kernel_eq_measure_prod MeasureTheory.Measure.set_lintegral_condKernel_eq_measure_prod + +lemma lintegral_condKernel (hf : Measurable f) : + ∫⁻ b, ∫⁻ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫⁻ x, f x ∂ρ := by + conv_rhs => rw [← compProd_fst_condKernel ρ] + rw [lintegral_compProd hf] +#align probability_theory.lintegral_cond_kernel MeasureTheory.Measure.lintegral_condKernel + +lemma set_lintegral_condKernel (hf : Measurable f) {s : Set β} + (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : + ∫⁻ b in s, ∫⁻ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst + = ∫⁻ x in s ×ˢ t, f x ∂ρ := by + conv_rhs => rw [← compProd_fst_condKernel ρ] + rw [set_lintegral_compProd hf hs ht] +#align probability_theory.set_lintegral_cond_kernel MeasureTheory.Measure.set_lintegral_condKernel + +lemma set_lintegral_condKernel_univ_right (hf : Measurable f) {s : Set β} + (hs : MeasurableSet s) : + ∫⁻ b in s, ∫⁻ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst + = ∫⁻ x in s ×ˢ Set.univ, f x ∂ρ := by + rw [← set_lintegral_condKernel hf hs MeasurableSet.univ]; simp_rw [Measure.restrict_univ] +#align probability_theory.set_lintegral_cond_kernel_univ_right MeasureTheory.Measure.set_lintegral_condKernel_univ_right + +lemma set_lintegral_condKernel_univ_left (hf : Measurable f) {t : Set Ω} + (ht : MeasurableSet t) : + ∫⁻ b, ∫⁻ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst + = ∫⁻ x in Set.univ ×ˢ t, f x ∂ρ := by + rw [← set_lintegral_condKernel hf MeasurableSet.univ ht]; simp_rw [Measure.restrict_univ] +#align probability_theory.set_lintegral_cond_kernel_univ_left MeasureTheory.Measure.set_lintegral_condKernel_univ_left + +end Lintegral + +section Integral + +variable {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] + {E : Type*} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] + +lemma _root_.MeasureTheory.AEStronglyMeasurable.integral_condKernel + (hf : AEStronglyMeasurable f ρ) : + AEStronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst := by + rw [← ρ.compProd_fst_condKernel] at hf + exact AEStronglyMeasurable.integral_kernel_compProd hf +#align measure_theory.ae_strongly_measurable.integral_cond_kernel MeasureTheory.AEStronglyMeasurable.integral_condKernel + +lemma integral_condKernel (hf : Integrable f ρ) : + ∫ b, ∫ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x, f x ∂ρ := by + conv_rhs => rw [← compProd_fst_condKernel ρ] + rw [← compProd_fst_condKernel ρ] at hf + rw [integral_compProd hf] +#align probability_theory.integral_cond_kernel MeasureTheory.Measure.integral_condKernel + +lemma set_integral_condKernel {s : Set β} (hs : MeasurableSet s) + {t : Set Ω} (ht : MeasurableSet t) (hf : IntegrableOn f (s ×ˢ t) ρ) : + ∫ b in s, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ := by + conv_rhs => rw [← compProd_fst_condKernel ρ] + rw [← compProd_fst_condKernel ρ] at hf + rw [set_integral_compProd hs ht hf] +#align probability_theory.set_integral_cond_kernel MeasureTheory.Measure.set_integral_condKernel + +lemma set_integral_condKernel_univ_right {s : Set β} (hs : MeasurableSet s) + (hf : IntegrableOn f (s ×ˢ Set.univ) ρ) : + ∫ b in s, ∫ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ Set.univ, f x ∂ρ := by + rw [← set_integral_condKernel hs MeasurableSet.univ hf]; simp_rw [Measure.restrict_univ] +#align probability_theory.set_integral_cond_kernel_univ_right MeasureTheory.Measure.set_integral_condKernel_univ_right + +lemma set_integral_condKernel_univ_left {t : Set Ω} (ht : MeasurableSet t) + (hf : IntegrableOn f (Set.univ ×ˢ t) ρ) : + ∫ b, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in Set.univ ×ˢ t, f x ∂ρ := by + rw [← set_integral_condKernel MeasurableSet.univ ht hf]; simp_rw [Measure.restrict_univ] +#align probability_theory.set_integral_cond_kernel_univ_left MeasureTheory.Measure.set_integral_condKernel_univ_left + +end Integral + +end MeasureTheory.Measure + +namespace MeasureTheory + +/-! ### Integrability + +We place these lemmas in the `MeasureTheory` namespace to enable dot notation. -/ + +open ProbabilityTheory + +variable {α Ω E F : Type*} {mα : MeasurableSpace α} [MeasurableSpace Ω] + [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] + [NormedAddCommGroup F] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] + +theorem AEStronglyMeasurable.ae_integrable_condKernel_iff {f : α × Ω → F} + (hf : AEStronglyMeasurable f ρ) : + (∀ᵐ a ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧ + Integrable (fun a ↦ ∫ ω, ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f ρ := by + rw [← ρ.compProd_fst_condKernel] at hf + conv_rhs => rw [← ρ.compProd_fst_condKernel] + rw [Measure.integrable_compProd_iff hf] +#align measure_theory.ae_strongly_measurable.ae_integrable_cond_kernel_iff MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff + +theorem Integrable.condKernel_ae {f : α × Ω → F} (hf_int : Integrable f ρ) : + ∀ᵐ a ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a) := by + have hf_ae : AEStronglyMeasurable f ρ := hf_int.1 + rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int + exact hf_int.1 +#align measure_theory.integrable.cond_kernel_ae MeasureTheory.Integrable.condKernel_ae + +theorem Integrable.integral_norm_condKernel {f : α × Ω → F} (hf_int : Integrable f ρ) : + Integrable (fun x ↦ ∫ y, ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst := by + have hf_ae : AEStronglyMeasurable f ρ := hf_int.1 + rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int + exact hf_int.2 +#align measure_theory.integrable.integral_norm_cond_kernel MeasureTheory.Integrable.integral_norm_condKernel + +theorem Integrable.norm_integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) : + Integrable (fun x ↦ ‖∫ y, f (x, y) ∂ρ.condKernel x‖) ρ.fst := by + refine hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm ?_ + refine Filter.eventually_of_forall fun x ↦ ?_ + rw [norm_norm] + refine (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm + exact integral_nonneg_of_ae (Filter.eventually_of_forall fun y ↦ norm_nonneg _) +#align measure_theory.integrable.norm_integral_cond_kernel MeasureTheory.Integrable.norm_integral_condKernel + +theorem Integrable.integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) : + Integrable (fun x ↦ ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst := + (integrable_norm_iff hf_int.1.integral_condKernel).mp hf_int.norm_integral_condKernel +#align measure_theory.integrable.integral_cond_kernel MeasureTheory.Integrable.integral_condKernel + +end MeasureTheory diff --git a/Mathlib/Probability/Kernel/Disintegration/Unique.lean b/Mathlib/Probability/Kernel/Disintegration/Unique.lean new file mode 100644 index 0000000000000..16ee273fbe27a --- /dev/null +++ b/Mathlib/Probability/Kernel/Disintegration/Unique.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2023 Kexing Ying. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kexing Ying, Rémy Degenne +-/ +import Mathlib.Probability.Kernel.Disintegration.Integral + +/-! +# Uniqueness of the conditional kernel + +We prove that the conditional kernels `ProbabilityTheory.kernel.condKernel` and +`MeasureTheory.Measure.condKernel` are almost everywhere unique. + +## Main statements + +* `ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd`: a.e. uniqueness of + `ProbabilityTheory.kernel.condKernel` +* `ProbabilityTheory.eq_condKernel_of_measure_eq_compProd`: a.e. uniqueness of + `MeasureTheory.Measure.condKernel` +* `ProbabilityTheory.kernel.condKernel_apply_eq_condKernel`: the kernel `condKernel` is almost + everywhere equal to the measure `condKernel`. +-/ + +open MeasureTheory Set Filter MeasurableSpace + +open scoped ENNReal MeasureTheory Topology ProbabilityTheory + +namespace ProbabilityTheory + +variable {α β Ω : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + +section Measure + +variable {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] + +/-! ### Uniqueness of `Measure.condKernel` + +The conditional kernel of a measure is unique almost everywhere. -/ + +/-- A s-finite kernel which satisfy the disintegration property of the given measure `ρ` is almost +everywhere equal to the disintegration kernel of `ρ` when evaluated on a measurable set. + +This theorem in the case of finite kernels is weaker than `eq_condKernel_of_measure_eq_compProd` +which asserts that the kernels are equal almost everywhere and not just on a given measurable +set. -/ +theorem eq_condKernel_of_measure_eq_compProd' (κ : kernel α Ω) [IsSFiniteKernel κ] + (hκ : ρ = ρ.fst ⊗ₘ κ) {s : Set Ω} (hs : MeasurableSet s) : + ∀ᵐ x ∂ρ.fst, κ x s = ρ.condKernel x s := by + refine ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite + (kernel.measurable_coe κ hs) (kernel.measurable_coe ρ.condKernel hs) (fun t ht _ ↦ ?_) + conv_rhs => rw [Measure.set_lintegral_condKernel_eq_measure_prod ht hs, hκ] + simp only [Measure.compProd_apply (ht.prod hs), Set.mem_prod, ← lintegral_indicator _ ht] + congr with x + by_cases hx : x ∈ t + all_goals simp [hx] + +/-- Auxiliary lemma for `eq_condKernel_of_measure_eq_compProd`. +Uniqueness of the disintegration kernel on ℝ. -/ +lemma eq_condKernel_of_measure_eq_compProd_real {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ] + (κ : kernel α ℝ) [IsFiniteKernel κ] (hκ : ρ = ρ.fst ⊗ₘ κ) : + ∀ᵐ x ∂ρ.fst, κ x = ρ.condKernel x := by + have huniv : ∀ᵐ x ∂ρ.fst, κ x Set.univ = ρ.condKernel x Set.univ := + eq_condKernel_of_measure_eq_compProd' κ hκ MeasurableSet.univ + suffices ∀ᵐ x ∂ρ.fst, ∀ ⦃t⦄, MeasurableSet t → κ x t = ρ.condKernel x t by + filter_upwards [this] with x hx + ext t ht; exact hx ht + apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat + Real.isPiSystem_Iic_rat + · simp + · simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff] + exact ae_all_iff.2 fun q ↦ eq_condKernel_of_measure_eq_compProd' κ hκ measurableSet_Iic + · filter_upwards [huniv] with x hxuniv t ht heq + rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _] + · refine ae_of_all _ (fun x f hdisj hf heq ↦ ?_) + rw [measure_iUnion hdisj hf, measure_iUnion hdisj hf] + exact tsum_congr heq + +/-- A finite kernel which satisfies the disintegration property is almost everywhere equal to the +disintegration kernel. -/ +theorem eq_condKernel_of_measure_eq_compProd (κ : kernel α Ω) [IsFiniteKernel κ] + (hκ : ρ = ρ.fst ⊗ₘ κ) : + ∀ᵐ x ∂ρ.fst, κ x = ρ.condKernel x := by + -- The idea is to transport the question to `ℝ` from `Ω` using `embeddingReal` + -- and then construct a measure on `α × ℝ` + let f := embeddingReal Ω + have hf := measurableEmbedding_embeddingReal Ω + set ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f) with hρ'def + have hρ' : ρ'.fst = ρ.fst := by + ext s hs + rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_apply] + exacts [rfl, Measurable.prod measurable_fst <| hf.measurable.comp measurable_snd, + measurable_fst hs, hs, hs] + have hρ'' : ∀ᵐ x ∂ρ.fst, kernel.map κ f hf.measurable x = ρ'.condKernel x := by + rw [← hρ'] + refine eq_condKernel_of_measure_eq_compProd_real (kernel.map κ f hf.measurable) ?_ + ext s hs + conv_lhs => rw [hρ'def, hκ] + rw [Measure.map_apply (measurable_id.prod_map hf.measurable) hs, hρ', + Measure.compProd_apply hs, Measure.compProd_apply (measurable_id.prod_map hf.measurable hs)] + congr with a + rw [kernel.map_apply'] + exacts [rfl, measurable_prod_mk_left hs] + suffices ∀ᵐ x ∂ρ.fst, ∀ s, MeasurableSet s → ρ'.condKernel x s = ρ.condKernel x (f ⁻¹' s) by + filter_upwards [hρ'', this] with x hx h + rw [kernel.map_apply] at hx + ext s hs + rw [← Set.preimage_image_eq s hf.injective, + ← Measure.map_apply hf.measurable <| hf.measurableSet_image.2 hs, hx, + h _ <| hf.measurableSet_image.2 hs] + suffices ρ.map (Prod.map id f) = (ρ.fst ⊗ₘ (kernel.map ρ.condKernel f hf.measurable)) by + rw [← hρ'] at this + have heq := eq_condKernel_of_measure_eq_compProd_real _ this + rw [hρ'] at heq + filter_upwards [heq] with x hx s hs + rw [← hx, kernel.map_apply, Measure.map_apply hf.measurable hs] + ext s hs + conv_lhs => rw [← ρ.compProd_fst_condKernel] + rw [Measure.compProd_apply hs, Measure.map_apply (measurable_id.prod_map hf.measurable) hs, + Measure.compProd_apply] + · congr with a + rw [kernel.map_apply'] + exacts [rfl, measurable_prod_mk_left hs] + · exact measurable_id.prod_map hf.measurable hs + +end Measure + +section KernelAndMeasure + +lemma kernel.apply_eq_measure_condKernel_of_compProd_eq + {ρ : kernel α (β × Ω)} [IsFiniteKernel ρ] {κ : kernel (α × β) Ω} [IsFiniteKernel κ] + (hκ : kernel.fst ρ ⊗ₖ κ = ρ) (a : α) : + (fun b ↦ κ (a, b)) =ᵐ[kernel.fst ρ a] (ρ a).condKernel := by + have : ρ a = (ρ a).fst ⊗ₘ kernel.comap κ (fun b ↦ (a, b)) measurable_prod_mk_left := by + ext s hs + conv_lhs => rw [← hκ] + rw [Measure.compProd_apply hs, kernel.compProd_apply _ _ _ hs] + rfl + have h := eq_condKernel_of_measure_eq_compProd _ this + rw [kernel.fst_apply] + filter_upwards [h] with b hb + rw [← hb, kernel.comap_apply] + +/-- For `fst κ a`-almost all `b`, the conditional kernel `kernel.condKernel κ` applied to `(a, b)` +is equal to the conditional kernel of the measure `κ a` applied to `b`. -/ +lemma kernel.condKernel_apply_eq_condKernel [CountableOrCountablyGenerated α β] + (κ : kernel α (β × Ω)) [IsFiniteKernel κ] (a : α) : + (fun b ↦ kernel.condKernel κ (a, b)) =ᵐ[kernel.fst κ a] (κ a).condKernel := + kernel.apply_eq_measure_condKernel_of_compProd_eq (compProd_fst_condKernel κ) a + +lemma condKernel_const [CountableOrCountablyGenerated α β] (ρ : Measure (β × Ω)) [IsFiniteMeasure ρ] + (a : α) : + (fun b ↦ kernel.condKernel (kernel.const α ρ) (a, b)) =ᵐ[ρ.fst] ρ.condKernel := by + have h := kernel.condKernel_apply_eq_condKernel (kernel.const α ρ) a + simp_rw [kernel.fst_apply, kernel.const_apply] at h + filter_upwards [h] with b hb using hb + +end KernelAndMeasure + +section Kernel + +/-! ### Uniqueness of `kernel.condKernel` + +The conditional kernel is unique almost everywhere. -/ + +/-- A finite kernel which satisfies the disintegration property is almost everywhere equal to the +disintegration kernel. -/ +theorem eq_condKernel_of_kernel_eq_compProd [CountableOrCountablyGenerated α β] + {ρ : kernel α (β × Ω)} [IsFiniteKernel ρ] {κ : kernel (α × β) Ω} [IsFiniteKernel κ] + (hκ : kernel.fst ρ ⊗ₖ κ = ρ) (a : α) : + ∀ᵐ x ∂(kernel.fst ρ a), κ (a, x) = kernel.condKernel ρ (a, x) := by + filter_upwards [kernel.condKernel_apply_eq_condKernel ρ a, + kernel.apply_eq_measure_condKernel_of_compProd_eq hκ a] with a h1 h2 + rw [h1, h2] + +end Kernel + +end ProbabilityTheory diff --git a/Mathlib/Probability/Kernel/IntegralCompProd.lean b/Mathlib/Probability/Kernel/IntegralCompProd.lean index a24f9f41c1178..ade5264b9505f 100644 --- a/Mathlib/Probability/Kernel/IntegralCompProd.lean +++ b/Mathlib/Probability/Kernel/IntegralCompProd.lean @@ -69,7 +69,7 @@ theorem integrable_kernel_prod_mk_left (a : α) {s : Set (β × γ)} (hs : Measu #align probability_theory.integrable_kernel_prod_mk_left ProbabilityTheory.integrable_kernel_prod_mk_left theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd [NormedSpace ℝ E] - [CompleteSpace E] ⦃f : β × γ → E⦄ (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) : + ⦃f : β × γ → E⦄ (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) : AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂η (a, x)) (κ a) := ⟨fun x => ∫ y, hf.mk f (x, y) ∂η (a, x), hf.stronglyMeasurable_mk.integral_kernel_prod_right'', by filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩ @@ -138,7 +138,7 @@ theorem _root_.MeasureTheory.Integrable.integral_norm_compProd ⦃f : β × γ ((integrable_compProd_iff hf.aestronglyMeasurable).mp hf).2 #align measure_theory.integrable.integral_norm_comp_prod MeasureTheory.Integrable.integral_norm_compProd -theorem _root_.MeasureTheory.Integrable.integral_compProd [NormedSpace ℝ E] [CompleteSpace E] +theorem _root_.MeasureTheory.Integrable.integral_compProd [NormedSpace ℝ E] ⦃f : β × γ → E⦄ (hf : Integrable f ((κ ⊗ₖ η) a)) : Integrable (fun x => ∫ y, f (x, y) ∂η (a, x)) (κ a) := Integrable.mono hf.integral_norm_compProd hf.aestronglyMeasurable.integral_kernel_compProd <| @@ -152,7 +152,7 @@ theorem _root_.MeasureTheory.Integrable.integral_compProd [NormedSpace ℝ E] [C /-! ### Bochner integral -/ -variable [NormedSpace ℝ E] [CompleteSpace E] {E' : Type*} [NormedAddCommGroup E'] +variable [NormedSpace ℝ E] {E' : Type*} [NormedAddCommGroup E'] [CompleteSpace E'] [NormedSpace ℝ E'] theorem kernel.integral_fn_integral_add ⦃f g : β × γ → E⦄ (F : E → E') @@ -244,6 +244,8 @@ theorem kernel.continuous_integral_integral : theorem integral_compProd : ∀ {f : β × γ → E} (_ : Integrable f ((κ ⊗ₖ η) a)), ∫ z, f z ∂(κ ⊗ₖ η) a = ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a := by + by_cases hE : CompleteSpace E; swap + · simp [integral, hE] apply Integrable.induction · intro c s hs h2s simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp, diff --git a/Mathlib/Probability/Kernel/MeasurableIntegral.lean b/Mathlib/Probability/Kernel/MeasurableIntegral.lean index 01593dd0cf7e5..96da308fc211f 100644 --- a/Mathlib/Probability/Kernel/MeasurableIntegral.lean +++ b/Mathlib/Probability/Kernel/MeasurableIntegral.lean @@ -253,12 +253,14 @@ open ProbabilityTheory ProbabilityTheory.kernel namespace MeasureTheory -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [IsSFiniteKernel κ] +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [IsSFiniteKernel κ] [IsSFiniteKernel η] theorem StronglyMeasurable.integral_kernel_prod_right ⦃f : α → β → E⦄ (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x => ∫ y, f x y ∂κ x := by classical + by_cases hE : CompleteSpace E; swap + · simp [integral, hE, stronglyMeasurable_const] borelize E haveI : TopologicalSpace.SeparableSpace (range (uncurry f) ∪ {0} : Set E) := hf.separableSpace_range_union_singleton diff --git a/Mathlib/Probability/Kernel/MeasureCompProd.lean b/Mathlib/Probability/Kernel/MeasureCompProd.lean index 9ef775fe51976..fd8d8d52fb4c6 100644 --- a/Mathlib/Probability/Kernel/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/MeasureCompProd.lean @@ -113,14 +113,14 @@ lemma integrable_compProd_iff [SFinite μ] [IsSFiniteKernel κ] {E : Type*} [Nor rfl lemma integral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*} - [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] + [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α × β → E} (hf : Integrable f (μ ⊗ₘ κ)) : ∫ x, f x ∂(μ ⊗ₘ κ) = ∫ a, ∫ b, f (a, b) ∂(κ a) ∂μ := by rw [compProd, ProbabilityTheory.integral_compProd hf] simp lemma set_integral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*} - [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] + [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) {f : α × β → E} (hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)) : ∫ x in s ×ˢ t, f x ∂(μ ⊗ₘ κ) = ∫ a in s, ∫ b in t, f (a, b) ∂(κ a) ∂μ := by