English
For a finite index set s and X_i, Var[∑ i∈s X_i; μ] = ∑ i∈s ∑ j∈s cov[X_i, X_j; μ] provided μ has finite measure and each X_i ∈ MemLp 2 μ.
Русский
Для конечного множества индексов s и переменных X_i: Var[∑ i∈s X_i; μ] = ∑ i∈s ∑ j∈s cov[X_i, X_j; μ].
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_sum' [IsFiniteMeasure μ] (hX : ∀ i ∈ s, MemLp (X i) 2 μ) :
Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ] :=
by
rw [← covariance_self, covariance_sum_left' (by simpa)]
· refine Finset.sum_congr rfl fun i hi ↦ ?_
rw [covariance_sum_right' (by simpa) (hX i hi)]
· exact memLp_finset_sum' _ (by simpa)
· exact (memLp_finset_sum' _ (by simpa)).aemeasurable
