variance_fun_sum' — Mathlib

English

Let μ be finite and s a finite index set; for X_i: ι → Ω → ℝ with MemLp 2 μ for all i ∈ s, Var[∑ i∈s X_i; μ] = ∑ i∈s ∑ j∈s cov[X_i, X_j; μ].

Русский

Пусть μ конечно, s конечен; X_i имеет конечный второй момент; Var[∑ X_i; μ] = ∑∑ cov.

LaTeX

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

Lean4

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

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