English
Let s ⊆ indices and t ⊆ indices be finite. Then Cov(∑_{i∈s} X_i, ∑_{j∈t} Y_j) = ∑_{i∈s} ∑_{j∈t} Cov(X_i, Y_j).
Русский
Пусть s и t — конечные подмножества индексов. Тогда Cov(∑_{i∈s} X_i, ∑_{j∈t} Y_j) = ∑_{i∈s} ∑_{j∈t} Cov(X_i, Y_j).
LaTeX
$$$\\operatorname{cov}_{\\mu}\\left(\\sum_{i\\in s} X_i, \\sum_{j\\in t} Y_j\\; ;\\; \\mu\\right) = \\sum_{i\\in s} \\sum_{j\\in t} \\operatorname{cov}_{\\mu}\\left(X_i, Y_j\\right)$$$
Lean4
theorem covariance_sum_sum' {ι' : Type*} {Y : ι' → Ω → ℝ} {t : Finset ι'} (hX : ∀ i ∈ s, MemLp (X i) 2 μ)
(hY : ∀ i ∈ t, MemLp (Y i) 2 μ) : cov[∑ i ∈ s, X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ] :=
by
rw [covariance_sum_left' hX]
· exact Finset.sum_congr rfl fun i hi ↦ by rw [covariance_sum_right' hY (hX i hi)]
· exact memLp_finset_sum' t hY
