integral_norm_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 integrable norm of the averaged kernel equals the norm of the integral against condDistrib Y X μ at X a.

Русский

Пусть hX, hY — AEMeasurable X, Y и hf_int — интегрируемый f по μ.map a ↦ (X a, Y a). Тогда интеграл нормы по кондDistrib совпадает с нормой интеграла против condDistrib(Y, X, μ) в X a.

LaTeX

$$$\\text{Integrable}_{a\\mapsto \\|\\int f(X(a), y)\\, d(\\operatorname{condDistrib}(Y,X,μ))(y)\\|} (μμ.map X).$$$

Lean4

theorem _root_.MeasureTheory.Integrable.integral_norm_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.integral_norm_condDistrib_map hY).comp_aemeasurable hX

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