covariance_comm

Mathlib.Probability.Moments.Covariance

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

English

Covariance is symmetric in its two random-variable arguments: cov(X, Y; μ) = cov(Y, X; μ).

Русский

Ковариация симметрична по аргументам-случайным величинам: cov(X, Y; μ) = cov(Y, X; μ).

LaTeX

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

Lean4

theorem covariance_comm : cov[X, Y; μ] = cov[Y, X; μ] :=
  by
  simp_rw [covariance]
  congr with x
  ring

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

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

Разделы

Аффилиация

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