covariance_add_const_left — Mathlib

English

Let X be integrable (under μ) and c be a real constant. Then cov[X + c, Z; μ] = cov[X, Z; μ].

Русский

Пусть X интегрируема по μ и константа c. Тогда cov[X + c, Z; μ] = cov[X, Z; μ].

LaTeX

$$$\operatorname{cov}(X \!+\! c, Z;\mu) = \operatorname{cov}(X, Z;\mu)$$$

Lean4

@[simp]
theorem covariance_add_const_left [IsProbabilityMeasure μ] (hX : Integrable X μ) (c : ℝ) :
    cov[fun ω ↦ X ω + c, Y; μ] = cov[X, Y; μ] := by
  simp_rw [covariance]
  congr with ω
  rw [integral_add hX (by fun_prop)]
  simp

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