Theorems · Theorem · dynamical systems

birkhoffSum_of_comp_eq

∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → α} {φ : α → M},
  φ ∘ f = φ → ∀ (n : ℕ), birkhoffSum f φ n = n • φ

If a function φ is invariant under a function f (i.e., φ ∘ f = φ), then the Birkhoff sum of φ over f for n iterations is equal to n • φ.

Defined in

Mathlib.Dynamics.BirkhoffSum.Basic

Cited by

1 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid