variance_fun_neg

Mathlib.Probability.Moments.Variance

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

English

Variance is invariant under negation: Var[−X; μ] = Var[X; μ].

Русский

Дисперсия не меняется при отрицании: Var[−X; μ] = Var[X; μ].

LaTeX

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

Lean4

theorem variance_fun_neg : Var[fun ω ↦ -X ω; μ] = Var[X; μ] :=
  by
  convert variance_mul (-1) X μ
  · ext; ring
  · simp

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

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

Разделы

Аффилиация

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