English
Let S and T be finite, f : S → M and g : T → M. If there exists a bijection i : S → T with f(s) = g(i(s)) for all s ∈ S, then the averages are equal: E_{s∈S} f(s) = E_{t∈T} g(t).
Русский
Пусть S и T конечны, f:S→M и g:T→M. Если существует биекция i:S→T такая, что f(s) = g(i(s)) для всех s ∈ S, тогда средние значения совпадают: E_{s∈S} f(s) = E_{t∈T} g(t).
LaTeX
$$$\exists i:S \to T\ (\text{bijective}) \wedge (\forall s\in S, f(s) = g(i(s))) \Rightarrow \dfrac{1}{|S|}\sum_{s\in S} f(s) = \dfrac{1}{|T|}\sum_{t\in T} g(t).$$$
Lean4
/-- Reorder an average.
The difference with `Finset.expect_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with `Finset.expect_bij` is that the bijection is a non-dependent function, rather
than being allowed to use membership of the domain of the average. -/
theorem expect_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (i_inj : (s : Set ι).InjOn i)
(i_surj : (s : Set ι).SurjOn i t) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]
