Documentation

Mathlib.Dynamics.BirkhoffSum.Basic

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
Instances For
    theorem birkhoffSum_zero {α : 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
    theorem birkhoffSum_one {α : 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
    theorem birkhoffSum_succ {α : 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 : ) (x : α) :
    birkhoffSum f g (n + 1) x = g x + birkhoffSum f g n (f x)
    theorem birkhoffSum_add {α : 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 Function.IsFixedPt.birkhoffSum_eq {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : αα} {x : α} (h : Function.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 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.