aestronglyMeasurable_integral_condDistrib

English

If AEStronglyMeasurable f has the appropriate map with condDistrib, then the integral over the conditional distribution defines an AEStronglyMeasurable function on the base measure.

Русский

Если функция f является AES сильной измеримой и имеет соответствующую форму с condDistrib, то интеграл по условному распределению задаёт AES измеримую функцию на базовой мере.

LaTeX

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

Lean4

theorem aestronglyMeasurable_integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable[mβ.comap X] (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ :=
  (hf.integral_condDistrib_map hY).comp_ae_measurable' hX

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