covariance_fun_sum_left — Mathlib

English

Let Fintype ι. If X_i ∈ L^2(μ) for all i and Y ∈ L^2(μ), then Cov(∑_{i} X_i, Y) = ∑_{i} Cov(X_i, Y).

Русский

Пусть ι конечен. Если для всех i X_i ∈ L^2(μ) и Y ∈ L^2(μ), то Cov(∑_i X_i, Y) = ∑_i Cov(X_i, Y).

LaTeX

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

Lean4

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

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