feat(Probability/Kernel): disintegration of finite kernels

[RemyDegenne]

trafficstars

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), there exists a kernel (α × β) Ω, called conditional kernel and denoted by kernel.condKernel κ such that κ = kernel.fst κ ⊗ₖ kernel.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 Q 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 CDFKernel.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 files Density.lean and KernelCDFReal.lean.

We define a class CountableOrCountablyGenerated α β which encodes the property (Countable α ∧ MeasurableSingletonClass α) ∨ CountablyGenerated β. The conditional kernel is defined under that assumption.

Properties of integrals involving kernel.condKernel are collated in the file Integral.lean. The conditional kernel is unique (almost everywhere w.r.t. kernel.fst κ): this is proved in the file Unique.lean.

---