covariance_neg_left — Mathlib

English

Covariance is linear with respect to negation on the left: cov(-X, Y; μ) = -cov(X, Y; μ).

Русский

Ковариация линейна по отношению к отрицанию слева: cov(-X, Y; μ) = -cov(X, Y; μ).

LaTeX

$$$\operatorname{cov}(-X, Y;\mu) = -\operatorname{cov}(X, Y;\mu)$$$

Lean4

@[simp]
theorem covariance_neg_left : cov[-X, Y; μ] = -cov[X, Y; μ] := by
  calc
    cov[-X, Y; μ]
    _ = cov[(-1 : ℝ) • X, Y; μ] := by simp
    _ = -cov[X, Y; μ] := by rw [covariance_smul_left]; simp

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