covariance_zero_right — Mathlib

English

Let X be a real-valued random variable on a probability space with measure μ. The covariance of X with the constant zero random variable is zero: cov(X, 0; μ) = 0.

Русский

Пусть X — вещественная случайная величина на вероятностном пространстве с мерой μ. Ковариация X с константой ноль равна нулю: cov(X, 0; μ) = 0.

LaTeX

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

Lean4

@[simp]
theorem covariance_zero_right : cov[X, 0; μ] = 0 := by simp [covariance]

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