variance_fun_sub — Mathlib

English

For MemLp X 2 μ and MemLp Y 2 μ, Var[X − Y; μ] equals 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_fun_sub [IsFiniteMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    Var[fun ω ↦ X ω - Y ω; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ] :=
  variance_sub hX hY

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