variance_zero

Mathlib.Probability.Moments.Variance

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.variance_zero

English

The variance of the zero function is zero: Var[0; μ] = 0 for any μ.

Русский

Дисперсия нулевой функции равна нулю: Var[0; μ] = 0 при любом μ.

LaTeX

$$$$ \mathrm{variance}(0, \mu) = 0. $$$$

Lean4

@[simp]
theorem variance_zero (μ : Measure Ω) : variance 0 μ = 0 := by simp only [variance, evariance_zero, ENNReal.toReal_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru