variance_fun_add — Mathlib

English

Under IsFiniteMeasure μ, for MemLp X 2 μ and MemLp Y 2 μ, Var[X + Y; μ] equals the same expansion as above.

Русский

При IsFiniteMeasure μ и X, Y соответствующих условиям Var[X+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_add [IsFiniteMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    Var[fun ω ↦ X ω + Y ω; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ] :=
  variance_add hX hY

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