covariance_sub_left — Mathlib

English

Covariance is additive in the left argument when forming X − Y: cov[X − Y, Z; μ] = cov[X, Z; μ] − cov[Y, Z; μ].

Русский

Ковариация аддитивна по левому аргументу при образовании X − Y: 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_sub_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 [sub_eq_add_neg, covariance_add_left hX hY.neg hZ, covariance_neg_left]

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