variance_fun_add — Mathlib

English

If a finite collection of real-valued random variables X_i are pairwise independent and each has finite second moment, then the variance of their sum equals the sum of their variances.

Русский

Пусть X_i — конечная совокупность случайных величин на Ω, попарно независимы и имеют конечный второй момент; тогда Var(∑ X_i) = ∑ Var(X_i).

LaTeX

$$$\operatorname{Var}\left[\sum_{i\in s} X_i; \; \mu\right] = \sum_{i\in s} \operatorname{Var}[X_i; \mu]$$$

Lean4

/-- The variance of the sum of two independent random variables is the sum of the variances. -/
theorem variance_fun_add {X Y : Ω → ℝ} (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) (h : IndepFun X Y μ) :
    Var[fun ω ↦ X ω + Y ω; μ] = Var[X; μ] + Var[Y; μ] :=
  h.variance_add hX hY

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