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 and measures #

Main definitions #

Main statements #

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

Disintegration of kernels on standard Borel spaces #

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