integral_condDistrib_map — Mathlib

English

Let hY be AEMeasurable Y μ and hf_int Integrable f with μ.map a ↦ (X a, Y a). Then ∫ y f(X a, y) d condDistrib(Y, X, μ) (X a) is integrable over a with respect to μ.map X.

Русский

Пусть hY — AE-измерима Y, hf_int интегрируемо f; тогда интеграл по y функции f(X a, y) против condDistrib(Y,X,μ) при X a интегрируем по a с μ.map X.

LaTeX

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

Lean4

theorem _root_.MeasureTheory.Integrable.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) :=
  (integrable_norm_iff (hf_int.1.integral_condDistrib_map hY)).mp (hf_int.norm_integral_condDistrib_map hY)

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