integrable_condExp — Mathlib

English

Under sigma-finite assumptions and AEStronglyMeasurable conditions, the ae equality between condExp and condExpL1CLM holds via a straight-line argument.

Русский

При сигма-конечности и условиях AEStronglyMeasurable равенство a.e. между CondExp и CondExpL1CLM следует по прямой схеме.

LaTeX

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

Lean4

@[fun_prop]
theorem integrable_condExp : Integrable (μ[f|m]) μ :=
  by
  by_cases hm : m ≤ m₀
  swap; · rw [condExp_of_not_le hm]; exact integrable_zero _ _ _
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · rw [condExp_of_not_sigmaFinite hm hμm]; exact integrable_zero _ _ _
  exact (integrable_condExpL1 f).congr (condExp_ae_eq_condExpL1 hm f).symm

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