covariance_fun_sum_right' — Mathlib

English

Let s be a finite set. If each X_i ∈ L^2(μ) for i∈s and Y ∈ L^2(μ), then Cov(Y, ∑_{i∈s} X_i) = ∑_{i∈s} Cov(Y, X_i).

Русский

Пусть s—конечное множество; если каждый X_i ∈ L^2(μ) и Y ∈ L^2(μ), то Cov(Y, ∑_{i∈s} X_i) = ∑_{i∈s} Cov(Y, X_i).

LaTeX

$$$\\operatorname{cov}_{\\mu}\\left(Y,\\sum_{i\\in s} X_i\\right) = \\sum_{i\\in s} \\operatorname{cov}_{\\mu}\\bigl(Y, X_i\\bigr)$$$

Lean4

theorem covariance_fun_sum_right' (hX : ∀ i ∈ s, MemLp (X i) 2 μ) (hY : MemLp Y 2 μ) :
    cov[Y, fun ω ↦ ∑ i ∈ s, X i ω; μ] = ∑ i ∈ s, cov[Y, X i; μ] :=
  by
  convert covariance_sum_right' hX hY
  simp

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