covariance_sum_sum — Mathlib

English

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

Русский

Пусть ι и ι' конечны. Тогда Cov(∑_ι X_i, ∑_{ι'} Y_j) = ∑_ι ∑_{ι'} Cov(X_i, Y_j).

LaTeX

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

Lean4

theorem covariance_sum_sum [Fintype ι] {ι' : Type*} [Fintype ι'] {Y : ι' → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ)
    (hY : ∀ i, MemLp (Y i) 2 μ) : cov[∑ i, X i, ∑ j, Y j; μ] = ∑ i, ∑ j, cov[X i, Y j; μ] :=
  covariance_sum_sum' (fun _ _ ↦ hX _) (fun _ _ ↦ hY _)

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