variance_smul' — Mathlib

English

For an algebra A over ℝ, and c ∈ A, variance scales as c^2 under the A-action: Var[c • X; μ] = c^2 • Var[X; μ].

Русский

Для алгебры A над ℝ и элемента c ∈ A дисперсия масштабируется по правилу c^2: 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' {A : Type*} [CommSemiring A] [Algebra A ℝ] (c : A) (X : Ω → ℝ) (μ : Measure Ω) :
    variance (c • X) μ = c ^ 2 • variance X μ :=
  by
  convert variance_smul (algebraMap A ℝ c) X μ using 1
  · simp only [algebraMap_smul]
  · simp only [Algebra.smul_def, map_pow]

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