variance_mul — Mathlib

English

For a real c and function X, Var[cX; μ] = c^2 Var[X; μ].

Русский

Для вещественного c и функции X: Var[cX; μ] = c^2 Var[X; μ].

LaTeX

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

Lean4

theorem variance_mul (c : ℝ) (X : Ω → ℝ) (μ : Measure Ω) : variance (fun ω => c * X ω) μ = c ^ 2 * variance X μ :=
  by
  rw [variance, evariance_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (sq_nonneg _)]
  rfl

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