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}
[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
- birkhoffSum f g n x = Finset.sum (Finset.range n) fun (k : ℕ) => g (f^[k] x)
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.