condExpL1_congr_ae — Mathlib

English

If f equals g almost everywhere with respect to μ, then their L1 conditional expectations are equal.

Русский

Если f совпадает с g почти повсеместно по μ, то их условные ожидания в L1 равны.

LaTeX

$$$f =_{a.e.\,μ} g\;\Rightarrow\; condExpL1 hm μ f = condExpL1 hm μ g$$$

Lean4

theorem condExpL1_congr_ae (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (h : f =ᵐ[μ] g) :
    condExpL1 hm μ f = condExpL1 hm μ g :=
  setToFun_congr_ae _ h

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