# Documentation

Mathlib.Probability.Kernel.Disintegration

# Disintegration of measures on product spaces #

Let ρ be a finite measure on α × Ω, where Ω is a standard Borel space. In mathlib terms, Ω verifies [Nonempty Ω] [TopologicalSpace Ω] [PolishSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]. 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, ρ = ((kernel.const Unit ρ.fst) ⊗ₖ (kernel.prodMkLeft Unit (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: ρ = ((kernel.const Unit ρ.fst) ⊗ₖ (kernel.prodMkLeft Unit ρ.condKernel)) ()
• ProbabilityTheory.eq_condKernel_of_measure_eq_compProd: a.e. uniqueness of condKernel

### Disintegration of measures on α × ℝ#

noncomputable def ProbabilityTheory.condKernelReal {α : Type u_1} {mα : } (ρ : ) :
{ x // }

Conditional measure on the second space of the product given the value on the first, as a kernel. Use the more general condKernel.

Instances For
theorem ProbabilityTheory.condKernelReal_Iic {α : Type u_1} {mα : } (ρ : ) (a : α) (x : ) :
↑() () = ENNReal.ofReal (↑() x)
theorem ProbabilityTheory.set_lintegral_condKernelReal_Iic {α : Type u_1} {mα : } (ρ : ) (x : ) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, ↑() () = ρ (s ×ˢ )
theorem ProbabilityTheory.set_lintegral_condKernelReal_univ {α : Type u_1} {mα : } (ρ : ) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, ↑() Set.univ = ρ (s ×ˢ Set.univ)
theorem ProbabilityTheory.lintegral_condKernelReal_univ {α : Type u_1} {mα : } (ρ : ) :
∫⁻ (a : α), ↑() Set.univ = ρ Set.univ
theorem ProbabilityTheory.set_lintegral_condKernelReal_prod {α : Type u_1} {mα : } (ρ : ) {s : Set α} (hs : ) {t : } (ht : ) :
∫⁻ (a : α) in s, ↑() t = ρ (s ×ˢ t)
theorem ProbabilityTheory.lintegral_condKernelReal_mem {α : Type u_1} {mα : } (ρ : ) {s : Set (α × )} (hs : ) :
∫⁻ (a : α), ↑() {x | (a, x) s} = ρ s
theorem ProbabilityTheory.kernel.const_eq_compProd_real {α : Type u_1} {mα : } (γ : Type u_2) [] (ρ : ) :
theorem ProbabilityTheory.measure_eq_compProd_real {α : Type u_1} {mα : } (ρ : ) :
theorem ProbabilityTheory.lintegral_condKernelReal {α : Type u_1} {mα : } (ρ : ) {f : α × ENNReal} (hf : ) :
∫⁻ (a : α), ∫⁻ (y : ), f (a, y) = ∫⁻ (x : α × ), f xρ
theorem ProbabilityTheory.ae_condKernelReal_eq_one {α : Type u_1} {mα : } (ρ : ) {s : } (hs : ) (hρ : ρ {x | x.snd s} = 0) :
∀ᵐ (a : α) ∂, ↑() s = 1

### Disintegration of measures on Polish Borel spaces #

Since every standard Borel space embeds measurably into ℝ, we can generalize the disintegration property on ℝ to all these spaces.

theorem ProbabilityTheory.exists_cond_kernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) (γ : Type u_3) [] :

Existence of a conditional kernel. Use the definition condKernel to get that kernel.

@[irreducible]
noncomputable def MeasureTheory.Measure.condKernel {α : Type u_3} {mα : } {Ω : Type u_4} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
{ x // }

Conditional kernel of a measure on a product space: a Markov kernel such that ρ = ((kernel.const Unit ρ.fst) ⊗ₖ (kernel.prodMkLeft Unit ρ.condKernel)) () (see ProbabilityTheory.measure_eq_compProd).

Instances For
theorem MeasureTheory.Measure.condKernel_def {α : Type u_3} {mα : } {Ω : Type u_4} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
= Exists.choose (_ : η _h, )
theorem ProbabilityTheory.condKernel_def {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
= Exists.choose (_ : η _h, )
instance ProbabilityTheory.instIsMarkovKernelCondKernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
theorem ProbabilityTheory.kernel.const_unit_eq_compProd {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
theorem ProbabilityTheory.measure_eq_compProd {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) :

Disintegration of finite product measures on α × Ω, where Ω is Polish 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 ProbabilityTheory.kernel.const_eq_compProd {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (γ : Type u_3) [] (ρ : MeasureTheory.Measure (α × Ω)) :

Disintegration of constant kernels. A constant kernel on a product space α × Ω, where Ω is Polish 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 ProbabilityTheory.lintegral_condKernel_mem {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) {s : Set (α × Ω)} (hs : ) :
∫⁻ (a : α), ↑() {x | (a, x) s} = ρ s
theorem ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) {s : Set α} (hs : ) {t : Set Ω} (ht : ) :
∫⁻ (a : α) in s, ↑() t = ρ (s ×ˢ t)
theorem ProbabilityTheory.lintegral_condKernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) {f : α × ΩENNReal} (hf : ) :
∫⁻ (a : α), ∫⁻ (ω : Ω), f (a, ω) = ∫⁻ (x : α × Ω), f xρ
theorem ProbabilityTheory.set_lintegral_condKernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) {f : α × ΩENNReal} (hf : ) {s : Set α} (hs : ) {t : Set Ω} (ht : ) :
∫⁻ (a : α) in s, ∫⁻ (ω : Ω) in t, f (a, ω) = ∫⁻ (x : α × Ω) in s ×ˢ t, f xρ
theorem ProbabilityTheory.set_lintegral_condKernel_univ_right {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) {f : α × ΩENNReal} (hf : ) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, ∫⁻ (ω : Ω), f (a, ω) = ∫⁻ (x : α × Ω) in s ×ˢ Set.univ, f xρ
theorem ProbabilityTheory.set_lintegral_condKernel_univ_left {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) {f : α × ΩENNReal} (hf : ) {t : Set Ω} (ht : ) :
∫⁻ (a : α), ∫⁻ (ω : Ω) in t, f (a, ω) = ∫⁻ (x : α × Ω) in Set.univ ×ˢ t, f xρ
theorem MeasureTheory.AEStronglyMeasurable.integral_condKernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] {E : Type u_3} [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y)) ()
theorem ProbabilityTheory.integral_condKernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] {E : Type u_3} [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} (hf : ) :
∫ (a : α), ∫ (x : Ω), f (a, x) = ∫ (ω : α × Ω), f ωρ
theorem ProbabilityTheory.set_integral_condKernel {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] {E : Type u_3} [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} {s : Set α} (hs : ) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t)) :
∫ (a : α) in s, ∫ (ω : Ω) in t, f (a, ω) = ∫ (x : α × Ω) in s ×ˢ t, f xρ
theorem ProbabilityTheory.set_integral_condKernel_univ_right {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] {E : Type u_3} [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} {s : Set α} (hs : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ)) :
∫ (a : α) in s, ∫ (ω : Ω), f (a, ω) = ∫ (x : α × Ω) in s ×ˢ Set.univ, f xρ
theorem ProbabilityTheory.set_integral_condKernel_univ_left {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] {E : Type u_3} [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t)) :
∫ (a : α), ∫ (ω : Ω) in t, f (a, ω) = ∫ (x : α × Ω) in Set.univ ×ˢ t, f xρ

### Uniqueness #

This section will prove that the conditional kernel is unique almost everywhere.

theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd' {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) (κ : { x // }) (hκ : ) {s : Set Ω} (hs : ) :
∀ᵐ (x : α) ∂, ↑(κ x) s = ↑() s

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 ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real {α : Type u_1} {mα : } (ρ : ) (κ : { x // }) (hκ : ) :
∀ᵐ (x : α) ∂, κ x =
theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd {α : Type u_1} {mα : } {Ω : Type u_2} [] [] [] [] [] (ρ : MeasureTheory.Measure (α × Ω)) (κ : { x // }) (hκ : ) :
∀ᵐ (x : α) ∂, κ x =

A finite kernel which satisfies the disintegration property is almost everywhere equal to the disintegration kernel.

### Integrability #

We place these lemmas in the MeasureTheory namespace to enable dot notation.

theorem MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : } [] [] [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩF} (hf : ) :
((∀ᵐ (a : α) ∂, MeasureTheory.Integrable fun ω => f (a, ω)) MeasureTheory.Integrable fun a => ∫ (ω : Ω), f (a, ω))
theorem MeasureTheory.Integrable.condKernel_ae {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : } [] [] [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩF} (hf_int : ) :
∀ᵐ (a : α) ∂, MeasureTheory.Integrable fun ω => f (a, ω)
theorem MeasureTheory.Integrable.integral_norm_condKernel {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : } [] [] [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩF} (hf_int : ) :
MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y)
theorem MeasureTheory.Integrable.norm_integral_condKernel {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : } [] [] [] [] [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} (hf_int : ) :
MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y)
theorem MeasureTheory.Integrable.integral_condKernel {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : } [] [] [] [] [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} (hf_int : ) :
MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y)