integral_condDistrib — Mathlib

English

If AEStronglyMeasurable f on ν and Y, X satisfy the measurability assumptions, then the map a ↦ ∫ f(X a, y) d condDistrib Y X μ (X a) is AEStronglyMeasurable on μ.map X.

Русский

Если f измеримо сильно AES на ν и Y, X удовлетворяют условиям измеримости, то функция a ↦ ∫ f(X(a), y) d condDistrib(Y,X,μ)(X(a)) измерима сильно AES относительно μ.map X.

LaTeX

$$$$\\text{AEStronglyMeasurable}(f, ν) \\implies \\text{AEStronglyMeasurable}(a \\mapsto \\int f(X(a), y) d condDistrib(Y,X,μ)(X(a)) , μ.map X).$$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ :=
  (hf.integral_condDistrib_map hY).comp_aemeasurable hX

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