norm_integral_condDistrib — Mathlib

English

Let hX and hY be AEMeasurable X, Y and hf_int Integrable f with μ.map a ↦ (X a, Y a). Then the integral of the norm of f(X a, ·) with respect to condDistrib Y X μ at X a is integrable with respect to μ.map X.

Русский

Пусть hf_int интегрируемо; тогда интеграл по ω нормы f(X(a), ω) по condDistrib(Y,X,μ) при X(a) интегрируем по μ.map X.

LaTeX

$$$\\text{Integrable}_{a}\\bigl(\\lambda a \\mapsto \\left\\| \\int_y f(X(a),y) d(\\operatorname{condDistrib}(Y,X,μ))(y) \\right\\|\\bigr)\\ (μ).$$$

Lean4

theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable (fun a => ‖∫ y, f (X a, y) ∂condDistrib Y X μ (X a)‖) μ :=
  (hf_int.norm_integral_condDistrib_map hY).comp_aemeasurable hX

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