variance_const_sub — Mathlib

English

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

Русский

Для IsProbabilityMeasure μ и AEStronglyMeasurable X, Var[c − X; μ] = Var[X; μ].

LaTeX

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

Lean4

theorem variance_const_sub [IsProbabilityMeasure μ] (hX : AEStronglyMeasurable X μ) (c : ℝ) :
    Var[fun ω ↦ c - X ω; μ] = Var[X; μ] := by
  simp_rw [sub_eq_add_neg]
  rw [variance_const_add (by fun_prop) c, variance_fun_neg]

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