covariance_fun_sum_fun_sum' — Mathlib

English

Let s and t be finite. Then Cov(∑_{i∈s} X_i, ∑_{j∈t} Y_j) = ∑_{i∈s} ∑_{j∈t} Cov(X_i, Y_j).

Русский

Пусть s и t — конечные. Тогда Cov(∑_{i∈s} X_i, ∑_{j∈t} Y_j) = ∑_{i∈s} ∑_{j∈t} Cov(X_i, Y_j).

LaTeX

$$$\\operatorname{cov}_{\\mu}\\left(\\sum_{i\\in s} X_i, \\sum_{j\\in t} Y_j\\right) = \\sum_{i\\in s} \\sum_{j\\in t} \\operatorname{cov}_{\\mu}\\left(X_i, Y_j\\right)$$$

Lean4

theorem covariance_fun_sum_fun_sum' {ι' : Type*} {Y : ι' → Ω → ℝ} {t : Finset ι'} (hX : ∀ i ∈ s, MemLp (X i) 2 μ)
    (hY : ∀ i ∈ t, MemLp (Y i) 2 μ) :
    cov[fun ω ↦ ∑ i ∈ s, X i ω, fun ω ↦ ∑ j ∈ t, Y j ω; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ] :=
  by
  convert covariance_sum_sum' hX hY
  all_goals simp

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