Birkhoff sums

In this file we define birkhoffSum f g n x to be the sum ∑ k ∈ Finset.range n, g (f^[k] x). This sum (more precisely, the corresponding average n⁻¹ • birkhoffSum f g n x) appears in various ergodic theorems saying that these averages converge to the "space average" ⨍ x, g x ∂μ in some sense.

See also birkhoffAverage defined in Dynamics/BirkhoffSum/Average.

def birkhoffSum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : M

The sum of values of g on the first n points of the orbit of x under f.

Equations

• birkhoffSum f g n x = ∑ k ∈ Finset.range n, g (f^[k] x)

theorem birkhoffSum_zero_apply {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (x : α) : birkhoffSum f g 0 x = 0

@[simp]

theorem birkhoffSum_zero {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) : birkhoffSum f g 0 = 0

@[deprecated birkhoffSum_zero (since := "2026-08-06")]

theorem birkhoffSum_zero' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) : birkhoffSum f g 0 = 0

Alias of birkhoffSum_zero.

theorem birkhoffSum_one_apply {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (x : α) : birkhoffSum f g 1 x = g x

@[simp]

theorem birkhoffSum_one {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) : birkhoffSum f g 1 = g

@[deprecated birkhoffSum_one (since := "2026-08-06")]

theorem birkhoffSum_one' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) : birkhoffSum f g 1 = g

Alias of birkhoffSum_one.

theorem birkhoffSum_succ_apply {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : birkhoffSum f g (n + 1) x = birkhoffSum f g n x + g (f^[n] x)

theorem birkhoffSum_succ {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) : birkhoffSum f g (n + 1) = birkhoffSum f g n + g ∘ f^[n]

theorem birkhoffSum_succ_apply' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : birkhoffSum f g (n + 1) x = g x + birkhoffSum f g n (f x)

theorem birkhoffSum_succ' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) : birkhoffSum f g (n + 1) = g + birkhoffSum f g n ∘ f

theorem birkhoffSum_add_apply {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g g' : α → M) (n : ℕ) (x : α) : birkhoffSum f (g + g') n x = birkhoffSum f g n x + birkhoffSum f g' n x

theorem birkhoffSum_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g g' : α → M) : birkhoffSum f (g + g') = birkhoffSum f g + birkhoffSum f g'

theorem birkhoffSum_add_right_apply {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (m n : ℕ) (x : α) : birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)

theorem birkhoffSum_add_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (m n : ℕ) : birkhoffSum f g (m + n) = birkhoffSum f g m + birkhoffSum f g n ∘ f^[m]

theorem Function.IsFixedPt.birkhoffSum_eq {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → α} {x : α} (h : IsFixedPt f x) (g : α → M) (n : ℕ) : birkhoffSum f g n x = n • g x

theorem map_birkhoffSum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {F : Type u_3} {N : Type u_4} [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α) : g' (birkhoffSum f g n x) = birkhoffSum f (⇑g' ∘ g) n x

theorem map_comp_birkhoffSum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {F : Type u_3} {N : Type u_4} [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) : ⇑g' ∘ birkhoffSum f g n = birkhoffSum f (⇑g' ∘ g) n

theorem birkhoffSum_comp_apply {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : birkhoffSum f (g ∘ f) n x = birkhoffSum f g n (f x)

theorem birkhoffSum_comp {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) : birkhoffSum f (g ∘ f) n = birkhoffSum f g n ∘ f

theorem birkhoffSum_apply_of_comp_eq {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → α} {φ : α → M} (h : φ ∘ f = φ) (n : ℕ) (x : α) : birkhoffSum f φ n x = n • φ x

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 • φ x at every point x.

theorem birkhoffSum_of_comp_eq {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → α} {φ : α → M} (h : φ ∘ 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 • φ.

theorem birkhoffSum_neg_apply {α : Type u_1} {G : Type u_2} [AddCommGroup G] (f : α → α) (g : α → G) (n : ℕ) (x : α) : birkhoffSum f (-g) n x = -birkhoffSum f g n x

theorem birkhoffSum_neg {α : Type u_1} {G : Type u_2} [AddCommGroup G] (f : α → α) (g : α → G) : birkhoffSum f (-g) = -birkhoffSum f g

theorem birkhoffSum_sub_apply {α : Type u_1} {G : Type u_2} [AddCommGroup G] (f : α → α) (g g' : α → G) (n : ℕ) (x : α) : birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x

theorem birkhoffSum_sub {α : Type u_1} {G : Type u_2} [AddCommGroup G] (f : α → α) (g g' : α → G) : birkhoffSum f (g - g') = birkhoffSum f g - birkhoffSum f g'

theorem birkhoffSum_apply_sub_birkhoffSum {α : Type u_1} {G : Type u_2} [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.

theorem birkhoffSum_comp_sub_birkhoffSum {α : Type u_1} {G : Type u_2} [AddCommGroup G] (f : α → α) (g : α → G) (n : ℕ) : birkhoffSum f g n ∘ f - birkhoffSum f g n = g ∘ f^[n] - g

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