condExpL2_ae_eq_condExp' — Mathlib

English

If f is integrable and MemLp f 2 μ, then the L2-conditional expectation equals the standard conditional expectation a.e.

Русский

Если f интегрируем и MemLp f 2 μ, то L2-условное ожидание равно обычному условному ожиданию почти наверняка.

LaTeX

$$$\operatorname{condExpL2} E \; 𝕜 hm hf^{\!toLp} =^{\mathrm{ae}}_{\mu} \mu[f|m]$$$

Lean4

theorem condExpL2_ae_eq_condExp' (hm : m ≤ m₀) (hf1 : Integrable f μ) (hf2 : MemLp f 2 μ) [SigmaFinite (μ.trim hm)] :
    condExpL2 E 𝕜 hm hf2.toLp =ᵐ[μ] μ[f|m] :=
  by
  refine
    ae_eq_condExp_of_forall_setIntegral_eq hm hf1
      (fun s hs htop ↦ integrableOn_condExpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_)
      (aestronglyMeasurable_condExpL2 hm _)
  rw [integral_condExpL2_eq hm (hf2.toLp _) hs htop.ne]
  refine setIntegral_congr_ae (hm _ hs) ?_
  filter_upwards [hf2.coeFn_toLp] with ω hω _ using hω

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