# 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 = ρ

### Disintegration of kernels from α to γ × ℝ for countably generated γ#

theorem ProbabilityTheory.kernel.isRatCondKernelCDFAux_density_Iic {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :
ProbabilityTheory.IsRatCondKernelCDFAux (fun (p : α × γ) (q : ) => ) κ
theorem ProbabilityTheory.kernel.isRatCondKernelCDF_density_Iic {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :
ProbabilityTheory.IsRatCondKernelCDF (fun (p : α × γ) (q : ) => ) κ

Taking the kernel density of intervals Iic q for q : ℚ gives a function with the property isRatCondKernelCDF.

noncomputable def ProbabilityTheory.kernel.condKernelCDF {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :

The conditional kernel CDF of a kernel κ : kernel α (γ × ℝ), where γ is countably generated.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ProbabilityTheory.kernel.isCondKernelCDF_condKernelCDF {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :
noncomputable def ProbabilityTheory.kernel.condKernelReal {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :
()

Auxiliary definition for ProbabilityTheory.kernel.condKernel. A conditional kernel for κ : kernel α (γ × ℝ) where γ is countably generated.

Equations
Instances For
instance ProbabilityTheory.kernel.instIsMarkovKernelCondKernelReal {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :
Equations
• =
theorem ProbabilityTheory.kernel.compProd_fst_condKernelReal {α : Type u_1} {γ : Type u_3} {mα : } {mγ : } (κ : ()) :
noncomputable def ProbabilityTheory.kernel.condKernelUnitReal {α : Type u_1} {mα : } (κ : ()) :
()

Auxiliary definition for MeasureTheory.Measure.condKernel and ProbabilityTheory.kernel.condKernel. A conditional kernel for κ : kernel Unit (α × ℝ).

Equations
Instances For
Equations
• =

### 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.

noncomputable def ProbabilityTheory.kernel.borelMarkovFromReal {α : Type u_1} {mα : } (Ω : Type u_5) [] [] (η : ) :
()

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ProbabilityTheory.kernel.borelMarkovFromReal_apply {α : Type u_1} {mα : } (Ω : Type u_5) [] [] (η : ) (a : α) :
= if (η a) = 0 then else
theorem ProbabilityTheory.kernel.borelMarkovFromReal_apply' {α : Type u_1} {mα : } (Ω : Type u_5) [] [] (η : ) (a : α) {s : Set Ω} (hs : ) :
s = if (η a) = 0 then (η a) else .indicator 1 ()
instance ProbabilityTheory.kernel.instIsSFiniteKernelBorelMarkovFromReal {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (η : ) :

When η is an s-finite kernel, borelMarkovFromReal Ω η is an s-finite kernel.

Equations
• =
instance ProbabilityTheory.kernel.instIsFiniteKernelBorelMarkovFromReal {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (η : ) :

When η is a finite kernel, borelMarkovFromReal Ω η is a finite kernel.

Equations
• =
instance ProbabilityTheory.kernel.instIsMarkovKernelBorelMarkovFromReal {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (η : ) :

When η is a Markov kernel, borelMarkovFromReal Ω η is a Markov kernel.

Equations
• =
theorem ProbabilityTheory.kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) (η : ()) (hη : ) :

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 κ' ⊗ₖ η) _.

theorem ProbabilityTheory.kernel.compProd_fst_borelMarkovFromReal {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) (η : ()) (hη : ) :

For κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable), the hypothesis hη is fst κ' ⊗ₖ η = κ'. With that hypothesis, fst κ ⊗ₖ borelMarkovFromReal κ η = κ.

noncomputable def ProbabilityTheory.kernel.condKernelBorel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : } {mγ : } [] [] (κ : (ProbabilityTheory.kernel α (γ × Ω))) :

Auxiliary definition for ProbabilityTheory.kernel.condKernel. A conditional kernel for κ : kernel α (γ × Ω) where γ is countably generated and Ω is standard Borel.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance ProbabilityTheory.kernel.instIsMarkovKernelCondKernelBorel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : } {mγ : } [] [] (κ : (ProbabilityTheory.kernel α (γ × Ω))) :
Equations
• =
theorem ProbabilityTheory.kernel.compProd_fst_condKernelBorel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : } {mγ : } [] [] (κ : (ProbabilityTheory.kernel α (γ × Ω))) :
noncomputable def ProbabilityTheory.kernel.condKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (κ : ()) :
()

Auxiliary definition for MeasureTheory.Measure.condKernel and ProbabilityTheory.kernel.condKernel. A conditional kernel for κ : kernel Unit (α × Ω) where Ω is standard Borel.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance ProbabilityTheory.kernel.instIsMarkovKernelCondKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (κ : ()) :
Equations
• =
theorem ProbabilityTheory.kernel.compProd_fst_condKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (κ : ()) :
@[irreducible]
noncomputable def MeasureTheory.Measure.condKernel {α : Type u_5} {Ω : Type u_6} {mα : } [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
()

Conditional kernel of a measure on a product space: a Markov kernel such that ρ = ρ.fst ⊗ₘ ρ.condKernel (see MeasureTheory.Measure.compProd_fst_condKernel).

Equations
Instances For
theorem MeasureTheory.Measure.condKernel_def {α : Type u_5} {Ω : Type u_6} {mα : } [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
ρ.condKernel = ProbabilityTheory.kernel.comap (fun (a : α) => ((), a))
theorem MeasureTheory.Measure.condKernel_apply {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (ρ : MeasureTheory.Measure (α × Ω)) (a : α) :
ρ.condKernel a =
instance MeasureTheory.Measure.instIsMarkovKernelCondKernel {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
Equations
• =
theorem MeasureTheory.Measure.compProd_fst_condKernel {α : Type u_1} {Ω : Type u_4} {mα : } [] [] (ρ : MeasureTheory.Measure (α × Ω)) :
ρ.fst.compProd ρ.condKernel = ρ

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.

theorem MeasureTheory.Measure.condKernel_apply_of_ne_zero_of_measurableSet {α : Type u_1} {Ω : Type u_4} {mα : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} {x : α} (hx : ρ.fst {x} 0) {s : Set Ω} (hs : ) :
(ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Auxiliary lemma for condKernel_apply_of_ne_zero.

theorem MeasureTheory.Measure.condKernel_apply_of_ne_zero {α : Type u_1} {Ω : Type u_4} {mα : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} {x : α} (hx : ρ.fst {x} 0) (s : Set Ω) :
(ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

If the singleton {x} has non-zero mass for ρ.fst, then for all s : Set Ω, ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) .

noncomputable def ProbabilityTheory.kernel.condKernelCountable {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :

Auxiliary definition for ProbabilityTheory.kernel.condKernel. A conditional kernel for κ : kernel α (β × Ω) where α is countable and Ω is standard Borel.

Equations
• = fun (p : α × β) => (κ p.1).condKernel p.2,
Instances For
theorem ProbabilityTheory.kernel.condKernelCountable_apply {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) (p : α × β) :
= (κ p.1).condKernel p.2
instance ProbabilityTheory.kernel.instIsMarkovKernelCondKernelCountable {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :
Equations
• =
theorem ProbabilityTheory.kernel.compProd_fst_condKernelCountable {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :
@[irreducible]
noncomputable def ProbabilityTheory.kernel.condKernel {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :

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.

Equations
Instances For
theorem ProbabilityTheory.kernel.condKernel_def {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :
instance ProbabilityTheory.kernel.instIsMarkovKernelCondKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :

condKernel κ is a Markov kernel.

Equations
• =
theorem ProbabilityTheory.kernel.compProd_fst_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) :

Disintegration of finite kernels. The composition-product of fst κ and condKernel κ is equal to κ.