English
Let X: α → β, Y: α → Ω, μ a finite measure on α, and f: β × Ω → F. If Y is almost everywhere measurable with respect to μ and f is integrable with respect to the push-forward μ.map a ↦ (X a, Y a), then for μ.map X-almost every b the function ω ↦ f(b, ω) is integrable with respect to the conditional distribution condDistrib(Y, X, μ) at b.
Русский
Пусть X: α → β, Y: α → Ω, μ — конечная мера на α, и f: β × Ω → F. Если Y — AEMeasurable относительно μ, и f интегрируем по мере μ.map a ↦ (X a, Y a), то почти для почти всех b по мере μ.map X функция ω ↦ f(b, ω) интегрируема относительно условного распределения condDistrib(Y, X, μ) в точке b.
LaTeX
$$$\\forall^{\\mathrm{a.e.}}\\ b\\;\\partial(\\mu\\circ X^{-1}),\\ \\text{Integrable}(\\,\\lambda \\omega:\\Omega, f(b,\\omega)\\,)(\\operatorname{condDistrib}(Y,X,\\mu)\\, b).$$$
Lean4
theorem _root_.MeasureTheory.Integrable.condDistrib_ae_map (hY : AEMeasurable Y μ)
(hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
∀ᵐ b ∂μ.map X, Integrable (fun ω => f (b, ω)) (condDistrib Y X μ b) := by
rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.condKernel_ae
