condExp_congr_ae — Mathlib

English

If f =ᵐ[μ] g, then their conditional expectations are equal after trimming μ by hm.

Русский

Если f =ᵐ[μ] g, то их условные ожидания совпадают после усечения μ по hm.

LaTeX

$$$$\\mu[f|m] =_{\\text{ae}} \\mu[g|m] \\text{ under trimmed measure } (\\mu.trim hm).$$$$

Lean4

@[gcongr]
theorem condExp_congr_ae (h : f =ᵐ[μ] g) : μ[f|m] =ᵐ[μ] μ[g|m] :=
  by
  by_cases hm : m ≤ m₀
  swap; · simp_rw [condExp_of_not_le hm]; rfl
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl
  exact
    (condExp_ae_eq_condExpL1 hm f).trans
      (Filter.EventuallyEq.trans (by rw [condExpL1_congr_ae hm h]) (condExp_ae_eq_condExpL1 hm g).symm)

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