covariance_eq_zero — Mathlib

English

If X and Y are independent in the sense of IndepFun and both belong to L^2(μ), then their covariance is zero.

Русский

Если X и Y независимы в смысле IndepFun и оба лежат в L^2(μ), то их ковариация равна нулю.

LaTeX

$$$\\operatorname{cov}[X, Y; \\mu] = 0$$

Lean4

theorem covariance_eq_zero (h : IndepFun X Y μ) (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) : cov[X, Y; μ] = 0 :=
  by
  by_cases h' : ∀ᵐ ω ∂μ, X ω = 0
  · refine integral_eq_zero_of_ae ?_
    filter_upwards [h'] with ω hω
    simp [hω, integral_eq_zero_of_ae h']
  have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
  rw [covariance_eq_sub hX hY, h.integral_mul_eq_mul_integral hX.aestronglyMeasurable hY.aestronglyMeasurable, sub_self]

Похожие утверждения