covariance_fun_sum_left' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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