English
If X and Y have finite second moments under IsFiniteMeasure μ, then Var[X + Y; μ] = Var[X; μ] + 2 cov[X, Y; μ] + Var[Y; μ].
Русский
Если X и Y имеют конечные моменты второго порядка, то Var[X+Y; μ] = Var[X; μ] + 2 cov[X, Y; μ] + Var[Y; μ].
LaTeX
$$$$ \mathrm{variance}(X + Y, \mu) = \mathrm{variance}(X, \mu) + 2 \cdot \mathrm{cov}(X, Y; \mu) + \mathrm{variance}(Y, \mu). $$$$
Lean4
theorem variance_add [IsFiniteMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
Var[X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ] :=
by
rw [← covariance_self, covariance_add_left hX hY (hX.add hY), covariance_add_right hX hX hY,
covariance_add_right hY hX hY, covariance_self, covariance_self, covariance_comm]
· ring
· exact hY.aemeasurable
· exact hX.aemeasurable
· exact hX.aemeasurable.add hY.aemeasurable
