English
AEStronglyMeasurable f on ν and Y, X with μ lead to an equivalence between almost everywhere integrability of f under the conditional distributions and the integrability under μ.
Русский
Пусть f асимптотно сильно измеримо на ν, а X, Y удовлетворяют условиям; тогда существует эквивалентность между интегрируемостью почти всюду относительно условных распределений и интегрируемостью относительно μ.
LaTeX
$$$$\\text{AEStronglyMeasurable}(f, ν) \\land \\text{...} \\iff \\text{Integrable}(f, μ)$$$$
Lean4
theorem _root_.MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff (hY : AEMeasurable Y μ)
(hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
(∀ᵐ a ∂μ.map X, Integrable (fun ω => f (a, ω)) (condDistrib Y X μ a)) ∧
Integrable (fun a => ∫ ω, ‖f (a, ω)‖ ∂condDistrib Y X μ a) (μ.map X) ↔
Integrable f (μ.map fun a => (X a, Y a)) :=
by rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hY]
