English
If a finite set S is inverted to S⁻¹ under a group-like operation, then the average over S⁻¹ of f equals the average over S of f composed with inversion: E_{i∈S⁻¹} f(i) = E_{i∈S} f(i⁻¹).
Русский
Если множество S конечное и перевернуть его оператором инверсии, то среднее по S⁻¹ от f равно среднему по S от f(инверсии): E_{i∈S⁻¹} f(i) = E_{i∈S} f(i⁻¹).
LaTeX
$$$\dfrac{1}{|S|}\sum_{i\in S^{-1}} f(i) = \dfrac{1}{|S|}\sum_{i\in S} f(i^{-1}).$$$
Lean4
@[simp]
theorem expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) :
𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ :=
expect_image inv_injective.injOn