English
Let S and T be finite index sets, f : S → M and g : T → M be valued in an additive module. If there exists a bijection h : S → T such that g(h(s)) = f(s) for all s ∈ S (equivalently, g = f ∘ h⁻¹), then the averages of f over S and g over T coincide, i.e. the mean value of f on S equals the mean value of g on T.
Русский
Пусть S и T — конечные множества индексов, f : S → M и g : T → M — функции в модуле M. Если существует биекция h : S → T такая, что g(h(s)) = f(s) для всех s ∈ S (то есть g = f ∘ h⁻¹), то средние значения функций совпадают: среднее f на S равно среднему значению g на T.
LaTeX
$$$\exists h:S \to T\ \big(\text{bijective}(h) \wedge g = f \circ h^{-1}\big) \Rightarrow \dfrac{1}{|S|}\sum_{i\in S} f(i) = \dfrac{1}{|T|}\sum_{j\in T} g(j)$$$$
Lean4
/-- Reorder an average.
The difference with `Finset.expect_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with `Finset.expect_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the averages, rather than being non-dependent functions. -/
theorem expect_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t) (hj : ∀ a ha, j a ha ∈ s)
(left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a)
(h : ∀ a ha, f a = g (i a ha)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h]
