variance_fun_sum — Mathlib

English

Let μ be finite and ι finite; if MemLp (X i) 2 μ for all i, then Var[∑ i, X_i; μ] equals the double covariance sum over i and j.

Русский

Пусть μ конечна, ι конечен; при условии MemLp для всех X_i, Var[∑ X_i; μ] равна двойной сумме ковариаций по i и j.

LaTeX

$$$$ \mathrm{variance}\left(\sum_{i} X_i, \mu\right) = \sum_{i} \sum_{j} \mathrm{cov}(X_i, X_j; \mu). $$$$

Lean4

theorem variance_fun_sum [IsFiniteMeasure μ] [Fintype ι] (hX : ∀ i, MemLp (X i) 2 μ) :
    Var[fun ω ↦ ∑ i, X i ω; μ] = ∑ i, ∑ j, cov[X i, X j; μ] :=
  by
  convert variance_sum hX
  simp

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