English
Specialization of the bijection result: if e is a bijection between finite index sets and f,g correspond via f(i) = g(e(i)), then the averages are equal.
Русский
Специализация результата по биекции: если 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_bijective` is a variant of `Finset.expect_bij` that accepts
`Function.Bijective`.
See `Function.Bijective.expect_comp` for a version without `h`. -/
theorem expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) :
𝔼 i, f i = 𝔼 i, g i :=
expect_nbij e (fun _ _ ↦ mem_univ _) (fun i _ ↦ h i) he.injective.injOn <| by simpa using he.surjective.surjOn _
