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 (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

theorem birkhoffAverage_one (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

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 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] (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

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

theorem birkhoffAverage_apply_sub_birkhoffAverage {α : Type u_1} {M : Type u_2} (R : Type u_3) [DivisionRing 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).