variance_sum — Mathlib

English

Let μ be finite, ι finite, and X_i have finite second moments; Var[∑ i, X_i; μ] = ∑ i ∑ j cov[X_i, X_j; μ].

Русский

Пусть μ конечно, ι конечен, и X_i имеют конечные моменты второго порядка; Var[∑ X_i; μ] = ∑∑ cov.

LaTeX

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

Lean4

theorem variance_sum [IsFiniteMeasure μ] [Fintype ι] (hX : ∀ i, MemLp (X i) 2 μ) :
    Var[∑ i, X i; μ] = ∑ i, ∑ j, cov[X i, X j; μ] :=
  variance_sum' (fun _ _ ↦ hX _)

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