English
Let s ⊆ ι and t ⊆ κ be finite, f : ι × κ → M. The joint average over s × t equals the iterated average: 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) :
𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j := by
simp only [expect, card_product, sum_product', smul_sum, mul_inv, mul_smul, Nat.cast_mul]
