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} [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
Instances For
    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 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).