condExp_of_not_sigmaFinite — Mathlib

English

If the restricted measure μtrim hm is not sigma-finite, then the conditional expectation μ[f|m] equals 0.

Русский

Если ограниченная мера μtrim hm не сигма- конечна, то условное ожидание μ[f|m] равно нулю.

LaTeX

$$$$\\text{If } \\Sigma\\text{Finite}(\\mu\\!/\\!\\hm) \\text{ fails, then } \\mu[f|m] = 0.$$$$

Lean4

theorem condExp_of_not_sigmaFinite (hm : m ≤ m₀) (hμm_not : ¬SigmaFinite (μ.trim hm)) : μ[f|m] = 0 := by
  rw [condExp, dif_pos hm, dif_neg]; push_neg; exact fun h => absurd h hμm_not

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