variance_sub — Mathlib

English

For finite measure μ and MemLp X 2 μ, MemLp Y 2 μ, Var[X - Y; μ] = Var[X; μ] − 2 cov[X, Y; μ] + Var[Y; μ].

Русский

При конечной мере μ и X, Y с м. моментами, Var[X - Y; μ] = Var[X; μ] − 2 cov[X, Y; μ] + Var[Y; μ].

LaTeX

$$$$ \mathrm{variance}(X - Y, \mu) = \mathrm{variance}(X, \mu) - 2 \mathrm{cov}(X, Y; \mu) + \mathrm{variance}(Y, \mu). $$$$

Lean4

theorem variance_sub [IsFiniteMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    Var[X - Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ] :=
  by
  rw [sub_eq_add_neg, variance_add hX hY.neg, variance_neg, covariance_neg_right]
  ring

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