covariance_mul_left

Mathlib.Probability.Moments.Covariance

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

English

For any real c, cov[c X, Y; μ] = c · cov[X, Y; μ].

Русский

Для любого числа c выполняется cov[c X, Y; μ] = c · cov[X, Y; μ].

LaTeX

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

Lean4

theorem covariance_mul_left (c : ℝ) : cov[fun ω ↦ c * X ω, Y; μ] = c * cov[X, Y; μ] :=
  covariance_smul_left c

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

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

Разделы

Аффилиация

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