condExp_ae_eq_condExpL1CLM — Mathlib

English

There is a correspondence between condExp with CLM (continuous linear map) and the a.e. equivalence of CondExpL1CLM.

Русский

Существует соответствие между CondExp с CLM и a.e. равенством CondExpL1CLM.

LaTeX

$$$$\\mu[f|m] =_{\\text{ae}} condExpL1CLM E hm μ (hf.toL1 f).$$$$

Lean4

theorem condExp_ae_eq_condExpL1CLM (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ) :
    μ[f|m] =ᵐ[μ] condExpL1CLM E hm μ (hf.toL1 f) :=
  by
  refine (condExp_ae_eq_condExpL1 hm f).trans (Eventually.of_forall fun x => ?_)
  rw [condExpL1_eq hf]

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