Theorems · Theorem · dynamical systems

birkhoffSum_apply_sub_birkhoffSum

∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] (f : α → α) (g : α → G) (n : ℕ) (x : α),
  birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x

Birkhoff sum is "almost invariant" under f: the difference between birkhoffSum f g n (f x) and birkhoffSum f g n x is equal to g (f^[n] x) - g x.

Defined in

Mathlib.Dynamics.BirkhoffSum.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroup