expect_comm — Mathlib

English

The average of a double sum equals the sum of averages: E_i∈s sum_{j∈t} f(i,j) = sum_{j∈t} E_i∈s f(i,j).

Русский

Среднее от двойной суммы равно сумме средних: E_i∈s sum_{j∈t} f(i,j) = sum_{j∈t} E_i∈s f(i,j).

LaTeX

$$$$ \\mathbb{E}_{i \\in s} \\sum_{j \\in t} f(i,j) = \\sum_{j \\in t} \\mathbb{E}_{i \\in s} f(i,j). $$$$

Lean4

theorem expect_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : 𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j :=
  by rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]

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