Birkhoff average

In this file we define birkhoffAverage f g n x to be $$ \frac{1}{n}\sum_{k=0}^{n-1}g(f^{[k]}(x)), $$ where f : α → α is a self-map on some type α, g : α → M is a function from α to a module over a division semiring R, and R is used to formalize division by n as (n : R)⁻¹ • _.

While we need an auxiliary division semiring R to define birkhoffAverage, the definition does not depend on the choice of R, see birkhoffAverage_congr_ring.

def birkhoffAverage (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : M

The average value of g on the first n points of the orbit of x under f, i.e. the Birkhoff sum ∑ k ∈ Finset.range n, g (f^[k] x) divided by n.

This average appears in many ergodic theorems which say that (birkhoffAverage R f g · x) converges to the "space average" ⨍ x, g x ∂μ as n → ∞.

We use an auxiliary [DivisionSemiring R] to define division by n. However, the definition does not depend on the choice of R, see birkhoffAverage_congr_ring.

Equations

• birkhoffAverage R f g n x = (↑n)⁻¹ • birkhoffSum f g n x

theorem birkhoffAverage_zero_apply (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) (x : α) : birkhoffAverage R f g 0 x = 0

@[simp]

theorem birkhoffAverage_zero (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) : birkhoffAverage R f g 0 = 0

@[deprecated birkhoffAverage_zero (since := "2026-08-19")]

theorem birkhoffAverage_zero' (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) : birkhoffAverage R f g 0 = 0

Alias of birkhoffAverage_zero.

theorem birkhoffAverage_one_apply (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) (x : α) : birkhoffAverage R f g 1 x = g x

@[simp]

theorem birkhoffAverage_one (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) : birkhoffAverage R f g 1 = g

@[deprecated birkhoffAverage_one (since := "2026-08-19")]

theorem birkhoffAverage_one' (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (f : α → α) (g : α → M) : birkhoffAverage R f g 1 = g

Alias of birkhoffAverage_one.

theorem map_birkhoffAverage (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) {F : Type u_5} {N : Type u_6} [DivisionSemiring S] [AddCommMonoid N] [Module S N] [FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α) : g' (birkhoffAverage R f g n x) = birkhoffAverage S f (⇑g' ∘ g) n x

theorem map_comp_birkhoffAverage (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) {F : Type u_5} {N : Type u_6} [DivisionSemiring S] [AddCommMonoid N] [Module S N] [FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) : ⇑g' ∘ birkhoffAverage R f g n = birkhoffAverage S f (⇑g' ∘ g) n

theorem birkhoffAverage_apply_congr_ring (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [DivisionSemiring S] [Module S M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : birkhoffAverage R f g n x = birkhoffAverage S f g n x

theorem birkhoffAverage_congr_ring (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [DivisionSemiring S] [Module S M] : birkhoffAverage R = birkhoffAverage S

@[deprecated birkhoffAverage_congr_ring (since := "2026-08-19")]

theorem birkhoffAverage_congr_ring' (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [DivisionSemiring S] [Module S M] : birkhoffAverage R = birkhoffAverage S

Alias of birkhoffAverage_congr_ring.

theorem Function.IsFixedPt.birkhoffAverage_eq (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] {f : α → α} {x : α} (h : IsFixedPt f x) (g : α → M) {n : ℕ} (hn : ↑n ≠ 0) : birkhoffAverage R f g n x = g x

theorem birkhoffAverage_add_apply (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] {f : α → α} {g g' : α → M} (n : ℕ) (x : α) : birkhoffAverage R f (g + g') n x = birkhoffAverage R f g n x + birkhoffAverage R f g' n x

@[deprecated birkhoffSum_add_apply (since := "2026-08-19")]

theorem birkhoffSum_add' {α : 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

Alias of birkhoffSum_add_apply.

theorem birkhoffAverage_add (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] {f : α → α} {g g' : α → M} : birkhoffAverage R f (g + g') = birkhoffAverage R f g + birkhoffAverage R f g'

theorem birkhoffAverage_apply_of_comp_eq (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] {f : α → α} {g : α → M} (h : g ∘ f = g) {n : ℕ} (hn : ↑n ≠ 0) (x : α) : birkhoffAverage R f g n x = g x

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 x at every point x. Requires that 0 < n.

theorem birkhoffAverage_of_comp_eq (R : Type u_1) {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommMonoid M] [Module R M] {f : α → α} {g : α → M} (h : g ∘ f = g) {n : ℕ} (hn : ↑n ≠ 0) : birkhoffAverage R f g n = g

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_neg_apply {R : Type u_1} {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommGroup M] [Module R M] {f : α → α} {g : α → M} (n : ℕ) (x : α) : birkhoffAverage R f (-g) n x = -birkhoffAverage R f g n x

theorem birkhoffAverage_neg {R : Type u_1} {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommGroup M] [Module R M] {f : α → α} {g : α → M} : birkhoffAverage R f (-g) = -birkhoffAverage R f g

theorem birkhoffAverage_sub_apply {R : Type u_1} {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommGroup M] [Module R M] {f : α → α} {g g' : α → M} (n : ℕ) (x : α) : birkhoffAverage R f (g - g') n x = birkhoffAverage R f g n x - birkhoffAverage R f g' n x

theorem birkhoffAverage_sub {R : Type u_1} {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommGroup M] [Module R M] {f : α → α} {g g' : α → M} : birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g'

theorem birkhoffAverage_apply_sub_birkhoffAverage {R : Type u_1} {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommGroup M] [Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α) : birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)

Birkhoff average is "almost invariant" under f: the difference between birkhoffAverage R f g n (f x) and birkhoffAverage R f g n x is equal to (n : R)⁻¹ • (g (f^[n] x) - g x).

theorem birkhoffAverage_comp_sub_birkhoffAverage {R : Type u_1} {α : Type u_2} {M : Type u_3} [DivisionSemiring R] [AddCommGroup M] [Module R M] (f : α → α) (g : α → M) (n : ℕ) : birkhoffAverage R f g n ∘ f - birkhoffAverage R f g n = (↑n)⁻¹ • (g ∘ f^[n] - g)

Birkhoff average is "almost invariant" under f: the difference between birkhoffAverage R f g n ∘ f and birkhoffAverage R f g n is equal to (n : R)⁻¹ • (g ∘ f^[n] - g).