covariance_fun_neg_right

Mathlib.Probability.Moments.Covariance

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.covariance_fun_neg_right

English

Covariance with negative of X on the left equals negative covariance: 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_fun_neg_right : cov[X, fun ω ↦ -Y ω; μ] = -cov[X, Y; μ] :=
  covariance_neg_right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru