expect_inv_index — Mathlib

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

Похожие утверждения