# Birkhoff sums #

In this file we define birkhoffSum f g n x to be the sum ∑ k in 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} [] (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} [] (f : αα) (g : αM) (x : α) :
birkhoffSum f g 0 x = 0
@[simp]
theorem birkhoffSum_zero' {α : Type u_1} {M : Type u_2} [] (f : αα) (g : αM) :
birkhoffSum f g 0 = 0
theorem birkhoffSum_one {α : Type u_1} {M : Type u_2} [] (f : αα) (g : αM) (x : α) :
birkhoffSum f g 1 x = g x
@[simp]
theorem birkhoffSum_one' {α : Type u_1} {M : Type u_2} [] (f : αα) (g : αM) :
birkhoffSum f g 1 = g
theorem birkhoffSum_succ {α : Type u_1} {M : Type u_2} [] (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} [] (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} [] (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} [] {f : αα} {x : α} (h : ) (g : αM) (n : ) :
birkhoffSum f g n x = n g x
theorem map_birkhoffSum {α : Type u_1} {M : Type u_2} [] {F : Type u_3} {N : Type u_4} [] [FunLike 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} [] (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.