English
Let e : ι ≃ κ be a bijection and hfg the corresponding matching of f and g as in an equivalence. Then the average of f over s equals the average of g over t.
Русский
Пусть e : ι ≃ κ — биекция, и пусть соответствие f и g задано согласованно через эквивалентность. Тогда среднее по s от f равно среднему по t от g.
LaTeX
$$$\exists e:\iota\simeq\kappa\,\big(\forall i, i\in s \leftrightarrow e(i)\in t\big) \wedge (\forall i\in s, f(i) = g(e(i))) \Rightarrow \dfrac{1}{|s|}\sum_{i\in s} f(i) = \dfrac{1}{|t|}\sum_{j\in t} g(j).$$$
Lean4
@[simp]
theorem card_smul_expect (s : Finset ι) (f : ι → M) : #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i :=
by
obtain rfl | hs := s.eq_empty_or_nonempty
· simp
· rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
exact mod_cast hs.card_ne_zero
