covariance_fun_sum_fun_sum — Mathlib

English

Let s be finite and t finite. Then Cov(∑_{i∈s} X_i, ∑_{j∈t} Y_j) equals ∑_{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 [Fintype ι] {ι' : Type*} [Fintype ι'] {Y : ι' → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ)
    (hY : ∀ i, MemLp (Y i) 2 μ) : cov[fun ω ↦ ∑ i, X i ω, fun ω ↦ ∑ j, Y j ω; μ] = ∑ i, ∑ j, cov[X i, Y j; μ] :=
  covariance_fun_sum_fun_sum' (fun _ _ ↦ hX _) (fun _ _ ↦ hY _)

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