English
A variant stating that for X, Y with measurability assumptions, the a.e. condExp equality holds with condDistrib Y X μ.
Русский
Вариант с условиями измеримости: a.e. condExp равен интегралу против condDistrib.
LaTeX
$$$$ \\text{condExp}_\\text{ae} = \\text{integral}(condDistrib) $$$$
Lean4
/-- Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies
`μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω)`.
It is defined as the conditional distribution of the identity given the identity, where the second
identity is understood as a map from `Ω` with the σ-algebra `mΩ` to `Ω` with σ-algebra `m ⊓ mΩ`.
We use `m ⊓ mΩ` instead of `m` to ensure that it is a sub-σ-algebra of `mΩ`. We then use
`Kernel.comap` to get a kernel from `m` to `mΩ` instead of from `m ⊓ mΩ` to `mΩ`. -/
noncomputable def condExpKernel :=
val_proj @wrapped✝.{}
