covariance_add_right — Mathlib

English

If μ is finite and X, Y, Z are square-integrable, then cov[X, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ].

Русский

Для конечной меры μ и X, Y, Z ∈ L2(μ) выполняется ковариация линейна по справа: 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_add_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
  rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]

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