English
Let X: α → β and Y: α → Ω be AEMeasurable with respect to μ, and f: β × Ω → F such that f is integrable under the push-forward μ.map a ↦ (X a, Y a). Then for μ-almost every a, the function ω ↦ f(X(a), ω) is integrable with respect to condDistrib(Y, X, μ) at X(a).
Русский
Пусть X: α → β и Y: α → Ω — AEMeasurable относительно μ, и f: β × Ω → F так, что f интегрируем по мере μ.map a ↦ (X a, Y a). Тогда для почти всех a по μ функция ω ↦ f(X(a), ω) интегрируема относительно condDistrib(Y, X, μ) в X(a).
LaTeX
$$$\\forall^{\\mathrm{a.e.}} a\\;\\partial\\mu,\\; \\operatorname{Integrable}(\\lambda \\omega, f(X(a),\\omega))\\,(\\operatorname{condDistrib}(Y,X,\\mu)\\ (X(a))).$$$
Lean4
theorem _root_.MeasureTheory.Integrable.condDistrib_ae (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
(hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
∀ᵐ a ∂μ, Integrable (fun ω => f (X a, ω)) (condDistrib Y X μ (X a)) :=
ae_of_ae_map hX (hf_int.condDistrib_ae_map hY)
