English
Let e : ι ≃ κ be a bijection between index sets, with s ⊆ ι and t ⊆ κ related by e. If f : ι → M and hfg ensures f(i) = g(e(i)) for i ∈ s, then the two finite averages are equal: E_{i∈s} f(i) = E_{j∈t} g(j).
Русский
Пусть e : ι ≃ κ — биекция между наборами индексов, связанные множества s и t. Если f : ι → M и hfg задаёт f(i) = g(e(i)) для i ∈ s, то
E_{i∈s} f(i) = E_{j∈t} g(j).
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
/-- `Finset.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
most arguments. -/
theorem expect_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]
