English
If μ is finite and X, Y, Z are square-integrable, then cov[X + Y, Z; μ] = cov[X, Z; μ] + cov[Y, Z; μ].
Русский
Для конечной меры μ и X, Y, Z ∈ L2(μ) выполняется ковариация линейна по слева: cov[X+Y, Z; μ] = cov[X, Z; μ] + cov[Y, Z; μ].
LaTeX
$$$\operatorname{cov}(X+Y, Z;\mu) = \operatorname{cov}(X, Z;\mu) + \operatorname{cov}(Y, Z;\mu)$$$
Lean4
theorem covariance_add_left [IsFiniteMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) (hZ : MemLp Z 2 μ) :
cov[X + Y, Z; μ] = cov[X, Z; μ] + cov[Y, Z; μ] :=
by
simp_rw [covariance, Pi.add_apply]
rw [← integral_add]
· congr with x
rw [integral_add (hX.integrable (by simp)) (hY.integrable (by simp))]
ring
· exact (hX.sub (memLp_const _)).integrable_mul (hZ.sub (memLp_const _))
· exact (hY.sub (memLp_const _)).integrable_mul (hZ.sub (memLp_const _))
