English
For IsProbabilityMeasure μ and X,Y ∈ L^2(μ), the covariance equals the integral of XY minus the product of the expectations.
Русский
При μ - вероятность, и X,Y ∈ L^2(μ) коварианта равна интегралу XY минус произведение E[X]E[Y].
LaTeX
$$$\\mathrm{cov}(X,Y;\\mu) = \\int X Y \\, d\\mu - \\left(\\int X \\, d\\mu\\right)\\left(\\int Y \\, d\\mu\\right)$$$
Lean4
theorem covariance_eq_sub [IsProbabilityMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
cov[X, Y; μ] = μ[X * Y] - μ[X] * μ[Y] :=
by
simp_rw [covariance, sub_mul, mul_sub]
repeat rw [integral_sub]
· simp_rw [integral_mul_const, integral_const_mul, integral_const, measureReal_univ_eq_one, one_smul]
simp
· exact hY.const_mul _ |>.integrable (by simp)
· exact integrable_const _
· exact hX.integrable_mul hY
· exact hX.mul_const _ |>.integrable (by simp)
· exact (hX.integrable_mul hY).sub (hX.mul_const _ |>.integrable (by simp))
· exact (hY.const_mul _ |>.integrable (by simp)).sub (integrable_const _)
