# Documentation

Mathlib.Dynamics.BirkhoffSum.Average

# 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} [] [] [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 in 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.

Instances For
theorem birkhoffAverage_zero (R : Type u_1) {α : Type u_2} {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [Module R M] (S : Type u_4) {F : Type u_5} {N : Type u_6} [] [] [Module S 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} [] [] [Module R M] (S : Type u_4) [] [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} [] [] [Module R M] (S : Type u_4) [] [Module S M] :
theorem Function.IsFixedPt.birkhoffAverage_eq (R : Type u_1) {α : Type u_2} {M : Type u_3} [] [] [Module R M] [] {f : αα} {x : α} (h : ) (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) [] [] [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).