condVar_of_not_le — Mathlib

English

If SigmaFinite(μ.trim hm) is assumed, but certain integrability fails, then Var[X; μ | m] equals 0 a.e.

Русский

Предполагая сигма-конечность μ.trim hm, но при отсутствии требуемой интегрируемости, Var[X; μ | m] равно 0 почти наверняка.

LaTeX

$$$ [SigmaFinite](μ.trim hm) \Rightarrow Var[X; μ | m] = 0 \text{ a.e.} $$$

Lean4

theorem condVar_of_not_le (hm : ¬m ≤ m₀) : Var[X; μ | m] = 0 := by rw [condVar, condExp_of_not_le hm]

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