English
Let hY be AEMeasurable Y with respect to μ and hf_int Integrable f with respect to μ.map a ↦ (X a, Y a). Then the integral of the norm, ∫ ‖f(x, y)‖ d condDistrib(Y, X, μ)(x) over x mapped by X is integrable with respect to μ.map X.
Русский
Пусть hY—the AE-измеримая часть Y относительно μ, а hf_int—инегрируемая f по μ.map a ↦ (X a, Y a). Тогда интеграл по x от ‖f(x, y)‖ по кондDistrib(Y, X, μ) является интегрируемым по μ.map X.
LaTeX
$$$\\operatorname{Integrable}_{x\\mapsto \\int \\|f(x,y)\\|\\, d(\\operatorname{condDistrib}(Y,X,\\mu))\\, (x)}\\ (\\mu\\circ X^{-1}).$$$
Lean4
theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib_map (hY : AEMeasurable Y μ)
(hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂condDistrib Y X μ x) (μ.map X) := by
rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.integral_norm_condKernel
