covariance_zero_measure

Mathlib.Probability.Moments.Covariance

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

English

Let μ be the zero measure on Ω. Then the covariance of X and Y with respect to μ is zero: cov(X, Y; 0) = 0.

Русский

Пусть μ — нулевая мера на Ω. Тогда ковариация X и Y по мере μ равна нулю: cov(X, Y; 0) = 0.

LaTeX

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

Lean4

@[simp]
theorem covariance_zero_measure : cov[X, Y; (0 : Measure Ω)] = 0 := by simp [covariance]

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

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

Разделы

Аффилиация

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