condExp_of_not_integrable — Mathlib

English

If f is not integrable, then μ[f|m] = 0.

Русский

Если f не интегрируемо, то μ[f|m] = 0.

LaTeX

$$$$\\text{If } \\neg \\operatorname{Integrable}(f,\\mu) \\text{ then } \\mu[f|m] = 0.$$$$

Lean4

theorem condExp_of_not_integrable (hf : ¬Integrable f μ) : μ[f|m] = 0 :=
  by
  by_cases hm : m ≤ m₀
  swap; · rw [condExp_of_not_le hm]
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · rw [condExp_of_not_sigmaFinite hm hμm]
  rw [condExp_of_sigmaFinite, if_neg hf]

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