condExp_ae_eq_integral_condDistrib

English

Another variant ensuring a.e. equality of conditional expectation with the integral against condDistrib.

Русский

Еще одно замечание об а.е. равенстве условного ожидания и интеграла против condDistrib.

LaTeX

$$$$ \\text{CondExpProd''} $$$$

Lean4

theorem condExp_ae_eq_integral_condDistrib [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X)
    (hY : AEMeasurable Y μ) {f : Ω → F} (hf : StronglyMeasurable f) (hf_int : Integrable (fun a => f (Y a)) μ) :
    μ[fun a => f (Y a)|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f y ∂condDistrib Y X μ (X a) :=
  condExp_prod_ae_eq_integral_condDistrib hX hY (hf.comp_measurable measurable_snd) hf_int

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