variance_const_add — Mathlib

English

For AEStronglyMeasurable X and real c, Var[c + X; μ] = Var[X; μ].

Русский

При AEStronglyMeasurable X и константе c дисперсия константного сдвига равна дисперсии X: Var[c + X; μ] = Var[X; μ].

LaTeX

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

Lean4

theorem variance_const_add [IsProbabilityMeasure μ] (hX : AEStronglyMeasurable X μ) (c : ℝ) :
    Var[fun ω ↦ c + X ω; μ] = Var[X; μ] := by simp_rw [add_comm c, variance_add_const hX c]

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