English
For a finite index set, the variance of the finite sum ∑ X_i equals the sum of variances whenever the X_i are pairwise independent and square integrable.
Русский
Для конечного индекса I дисперсия суммы ∑ X_i равна сумме дисперсий, если переменные 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 a finite sum of pairwise independent random variables is the sum of the
variances. -/
nonrec theorem variance_sum {ι : Type*} {X : ι → Ω → ℝ} {s : Finset ι} (hs : ∀ i ∈ s, MemLp (X i) 2 μ)
(h : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j) μ) : variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, variance (X i) μ :=
by
by_cases h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
· rw [variance_congr (Y := 0), variance_zero]
· symm
refine Finset.sum_eq_zero fun i hi ↦ ?_
simp [variance_congr (h'' i hi)]
· have := fun (i : s) ↦ h'' i.1 i.2
filter_upwards [ae_all_iff.2 this] with ω hω
simp only [sum_apply, Pi.zero_apply]
exact Finset.sum_eq_zero fun i hi ↦ hω ⟨i, hi⟩
obtain ⟨j, hj1, hj2⟩ := not_forall₂.1 h''
obtain rfl | h' := s.eq_singleton_or_nontrivial hj1
· simp
obtain ⟨k, hk1, hk2⟩ := h'.exists_ne j
have := (hs j hj1).isProbabilityMeasure_of_indepFun (X j) (X k) (by simp) (by simp) hj2 (h hj1 hk1 hk2.symm)
rw [variance_sum' hs]
refine Finset.sum_congr rfl (fun i hi ↦ ?_)
rw [← covariance_self (hs i hi).aemeasurable]
refine Finset.sum_eq_single_of_mem i hi fun j hj1 hj2 ↦ ?_
exact (h hi hj1 hj2.symm).covariance_eq_zero (hs i hi) (hs j hj1)
