covariance_const_sub_right — Mathlib

English

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

Русский

Ковариация с c − Y справа равна −cov(X,Y; μ): cov[X, c − Y; μ] = −cov[X, Y; μ].

LaTeX

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

Lean4

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

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