English
Let s ⊆ ι and t ⊆ κ be finite sets and f : ι × κ → M. The average over the product set s × t equals the iterated average, i.e. E_{(i,j)∈s×t} f(i,j) = E_{i∈s} E_{j∈t} f(i,j).
Русский
Пусть s ⊆ ι и t ⊆ κ конечны, f : ι × κ → M. Среднее по произведению s × t равно вложенному среднему: E_{(i,j)∈s×t} f(i,j) = E_{i∈s} E_{j∈t} f(i,j).
LaTeX
$$$\mathbb{E}_{(i,j)\in s\times t} f(i,j) = \mathbb{E}_{i\in s}\,\mathbb{E}_{j\in t} f(i,j).$$$
Lean4
/-- Expectation over a product set equals the expectation of the fiberwise expectations.
For rewriting in the reverse direction, use `Finset.expect_product'`. -/
theorem expect_product (s : Finset ι) (t : Finset κ) (f : ι × κ → M) : 𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j) :=
by simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]
