covariance_const_add_right — Mathlib

English

If μ is a probability measure, Cov[X, c + Y; μ] = Cov[X, Y; μ] for integrable Y.

Русский

Если μ — вероятность, Cov[X, c + Y; μ] = Cov[X, Y; μ] при интегрируемости Y.

LaTeX

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

Lean4

@[simp]
theorem covariance_const_add_right [IsProbabilityMeasure μ] (hY : Integrable Y μ) (c : ℝ) :
    cov[X, fun ω ↦ c + Y ω; μ] = cov[X, Y; μ] := by
  simp_rw [add_comm c]
  exact covariance_add_const_right hY c

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