covariance_sub_const_right — Mathlib

English

Covariance with c − X on the left equals the negative of Cov(X,Y; μ): cov[c − X, Y; μ] = −cov[X, Y; μ].

Русский

Ковариация с c − X слева равна противоположной ковариации: cov[c − X, Y; μ] = −cov[X, Y; μ].

LaTeX

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

Lean4

@[simp]
theorem covariance_sub_const_right [IsProbabilityMeasure μ] (hY : Integrable Y μ) (c : ℝ) :
    cov[X, fun ω ↦ Y ω - c; μ] = cov[X, Y; μ] := by simp [sub_eq_add_neg, hY]

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