norm_integral_condDistrib_map — Mathlib

English

If hX and hY are AEMeasurable and hf_int Integrable, then the norm of the integral against condDistrib Y X μ is integrable with respect to μ.map X.

Русский

Если hX и hY — AEMeasurable, а hf_int интегрируем, то норма интеграла против condDistrib(Y,X,μ) по x интегрируема по μ.map X.

LaTeX

$$$\\text{Integrable}\\left(x\\mapsto \\left\\|\\int_y f(x,y)\\, d(\\operatorname{condDistrib}(Y,X,μ))(y)\\right\\|\\right)\\ (μ\\circ X^{-1}).$$$

Lean4

theorem _root_.MeasureTheory.Integrable.norm_integral_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.norm_integral_condKernel

Похожие утверждения