English
Specialization using an equivalence e: ι ≃ κ that automatically fills in parameters: if f,g satisfy f(i) = g(e(i)) then the averages agree.
Русский
Специализация с использованием эквивалентности e: ι ≃ κ, автоматическое заполнение параметров: если f(i) = g(e(i)), то средние совпадают.
LaTeX
$$$\mathbb{E}_{i} f(i) = \mathbb{E}_{i} g(i)$, при условии $f(i) = g(e(i))$ для эквивалентности $e$.$$
Lean4
/-- `Fintype.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
most arguments.
See `Equiv.expect_comp` for a version without `h`. -/
theorem expect_equiv (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i :=
expect_bijective _ e.bijective f g h
