variance_smul

Mathlib.Probability.Moments.Variance

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

English

For a real c, the variance of c • X equals c^2 times the variance of X: Var[c • X; μ] = c^2 Var[X; μ].

Русский

Дисперсия при умножении на скаляр: Var[c • X; μ] = c^2 Var[X; μ].

LaTeX

$$$$ \mathrm{variance}(c \cdot X, \mu) = c^2 \cdot \mathrm{variance}(X, \mu). $$$$

Lean4

theorem variance_smul (c : ℝ) (X : Ω → ℝ) (μ : Measure Ω) : variance (c • X) μ = c ^ 2 * variance X μ :=
  variance_mul c X μ

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

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

Разделы

Аффилиация

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