English
Let s ⊆ ι and t ⊆ κ be finite. Then the average of the product f(i) g(j) over i∈s, j∈t equals the product of the averages: E_{i∈s} E_{j∈t} f(i) g(j) = (E_{i∈s} f(i)) (E_{j∈t} g(j)).
Русский
Пусть s ⊆ ι, t ⊆ κ конечны. Тогда среднее произведения f(i) g(j) по i∈s, j∈t равно произведению средних: E_{i∈s}E_{j∈t} f(i)g(j) = (E_{i∈s} f(i))(E_{j∈t} g(j)).
LaTeX
$$$\mathbb{E}_{i\in s}\mathbb{E}_{j\in t} (f(i)\,g(j)) = \big(\mathbb{E}_{i\in s} f(i)\big)\big(\mathbb{E}_{j\in t} g(j)\big).$$$
Lean4
theorem expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι) (t : Finset κ) (f : ι → M)
(g : κ → M) : (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j := by simp_rw [expect_mul, mul_expect]
