English
Let S and T be finite, f : S → M and g : T → M. If there exists a bijection i : S → T such that f(s) = g(i(s)) for all s ∈ S, then the averages coincide as in the previous bijection case.
Русский
Пусть S и T конечны, f:S→M и g:T→M. Если существует биекция i:S→T такая, что f(s) = g(i(s)) для всех s ∈ S, то средние значения совпадают.
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 with an inverse, rather
than as a surjective injection.
The difference with `Finset.expect_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the averages.
The difference with `Finset.expect_equiv` is that bijectivity is only required to hold on the
domains of the averages, rather than on the entire types. -/
theorem expect_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
(left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) :
𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
simp_rw [expect, card_nbij' i j hi hj left_inv right_inv, sum_nbij' i j hi hj left_inv right_inv h]
