variance_sub_const — Mathlib

English

For IsProbabilityMeasure μ and AEStronglyMeasurable X, Var[X − c; μ] = Var[X; μ].

Русский

При IsProbabilityMeasure μ и AEStronglyMeasurable X, Var[X − c; μ] = Var[X; μ].

LaTeX

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

Lean4

theorem variance_sub_const [IsProbabilityMeasure μ] (hX : AEStronglyMeasurable X μ) (c : ℝ) :
    Var[fun ω ↦ X ω - c; μ] = Var[X; μ] := by simp_rw [sub_eq_add_neg, variance_add_const hX (-c)]

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