English
The conditional-expectation kernel condExpKernel μ m is a Markov kernel: for each ω, the measure condExpKernel μ m ω is a probability measure on Ω, and the assignment ω ↦ condExpKernel μ m ω is measurable with respect to the base σ-algebra.
Русский
Ядро условного математического ожидания condExpKernel μ m является Марковским ядром: для каждого ω мера condExpKernel μ m ω является вероятностной мерой на Ω, и отображение ω ↦ condExpKernel μ m ω является измеримым по базовой σ-алгебе.
LaTeX
$$$(condExpKernel)_{\\mu,m}:\\Omega\\to\\mathcal P(\\Omega)\\quad\\text{is a Markov kernel, i.e. }\\forall \\omega, (condExpKernel)_{\\mu,m}(\\omega)\\in\\mathcal P(\\Omega) \\text{ and } \\omega\\mapsto (condExpKernel)_{\\mu,m}(\\omega)(A)\\text{ is measurable for all }A\\in mΩ$$$
Lean4
instance : IsMarkovKernel (condExpKernel μ m) :=
by
rcases isEmpty_or_nonempty Ω with h | h
· exact ⟨fun a ↦ (IsEmpty.false a).elim⟩
· simpa [condExpKernel, h] using by infer_instance
