condExpL2_ae_eq_condExp — Mathlib

English

If certain measurability and integrability conditions hold, the L2 conditional expectation equals the conditional expectation almost everywhere.

Русский

При соблюдении условий измеримости и интегрируемости L2 условное ожидание равно условному ожиданию почти повсюду.

LaTeX

$$$\\operatorname{condExpL2} E 𝕜 hm hf =^{\\mu} \\operatorname{condExp} m \\mu f$$$

Lean4

theorem condExpL2_ae_eq_condExp (hm : m ≤ m₀) (hf : MemLp f 2 μ) [IsFiniteMeasure μ] :
    condExpL2 E 𝕜 hm hf.toLp =ᵐ[μ] μ[f|m] :=
  hf.condExpL2_ae_eq_condExp' hm (memLp_one_iff_integrable.1 <| hf.mono_exponent one_le_two)

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