covariance_sub_right — Mathlib

English

Covariance is additive in the right argument for Y − Z: cov[X, Y − Z; μ] = cov[X, Y; μ] − cov[X, Z; μ].

Русский

Ковариация аддитивна по правому аргументу для Y − Z: cov[X, Y − Z; μ] = cov[X, Y; μ] − cov[X, Z; μ].

LaTeX

$$$\operatorname{cov}(X, Y - Z;\mu) = \operatorname{cov}(X, Y;\mu) - \operatorname{cov}(X, Z;\mu)$$$

Lean4

theorem covariance_sub_right [IsFiniteMeasure μ] (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) (hZ : MemLp Z 2 μ) :
    cov[X, Y - Z; μ] = cov[X, Y; μ] - cov[X, Z; μ] := by
  simp_rw [sub_eq_add_neg, covariance_add_right hX hY hZ.neg, covariance_neg_right]

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