English
Let s be finite and f be M-valued. Then the n-th power of the average equals the average of the n-fold products over the n-fold indexing: (E_{i∈s} f(i))^n = E_{p∈Fintype.piFinset} ∏_{i} f(p(i)).
Русский
Пусть s конечен, и f: s → M. Тогда n-ая ступенька среднего равна среднему по n-мерной индексации произведения значений: (E_{i∈s} f(i))^n = E_{p∈Fintype.piFinset} ∏_{i} f(p(i)).
LaTeX
$$$\left(\mathbb{E}_{i\in s} f(i)\right)^n = \mathbb{E}_{p\in Fintype.piFinset} \prod_{i=1}^{n} f(p(i)).$$$
Lean4
theorem expect_pow (s : Finset ι) (f : ι → M) (n : ℕ) :
(𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i) := by
classical rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
