English
A simp variant stating birkhoffAverage R f g 1 = g; i.e., the one-step average equals the current value.
Русский
Упрощенная формулировка: birkhoffAverage R f g 1 = g.
LaTeX
$$$\mathrm{birkhoffAverage}(R,f,g,1) = g$$$
Lean4
/-- If a function `g` is invariant under a function `f` (i.e., `g ∘ f = g`), then the Birkhoff
average of `g` over `f` for `n` iterations is equal to `g`. Requires that `0 < n`. -/
theorem birkhoffAverage_of_comp_eq [CharZero R] {f : α → α} {g : α → M} (h : g ∘ f = g) {n : ℕ} (hn : n ≠ 0) :
birkhoffAverage R f g n = g := by
funext x
suffices (n : R)⁻¹ • n • g x = g x by simpa [birkhoffAverage, birkhoffSum_of_comp_eq h]
rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ (by norm_cast), one_smul]