Commit 2024-04-16 12:43 bde5669a
View on Github →feat(Probability/Kernel): disintegration of finite kernels (#10603)
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 κ
.
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
.