English
Let {X_i}_{i∈s} and Y be square-integrable random variables with respect to μ, where s is a finite index set. Then the covariance of the sum ∑_{i∈s} X_i with Y equals the sum of the covariances cov(X_i, Y) over i∈s.
Русский
Пусть для конечного множества индексов s имеются случайные величины X_i (i∈s) и Y такие, что X_i ⟂ L^2(μ) и Y ∈ L^2(μ). Тогда ковариация между суммой ∑_{i∈s} X_i и Y равна сумме ковариаций cov(X_i, Y) по i∈s.
LaTeX
$$$\\operatorname{cov}_{\\mu}\\left(\\sum_{i\\in s} X_i, Y\\right) = \\sum_{i\\in s} \\operatorname{cov}_{\\mu}\\bigl(X_i, Y\\bigr) $$$
Lean4
theorem covariance_sum_left' (hX : ∀ i ∈ s, MemLp (X i) 2 μ) (hY : MemLp Y 2 μ) :
cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ] := by
classical
induction s using Finset.induction with
| empty => simp
| insert i s hi
h_ind =>
rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
· exact fun j hj ↦ hX j (by simp [hj])
· exact hX i (by simp)
· exact memLp_finset_sum' s (fun j hj ↦ hX j (by simp [hj]))
· exact hY
