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
- birkhoffSum f g n x = ∑ k ∈ Finset.range n, g (f^[k] x)
Instances For
theorem
birkhoffSum_zero
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → α)
(g : α → M)
(x : α)
:
@[simp]
theorem
birkhoffSum_one
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → α)
(g : α → M)
(x : α)
:
@[simp]
theorem
birkhoffSum_succ
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → α)
(g : α → M)
(n : ℕ)
(x : α)
:
theorem
birkhoffSum_succ'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → α)
(g : α → M)
(n : ℕ)
(x : α)
:
theorem
birkhoffSum_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → α)
(g : α → M)
(m n : ℕ)
(x : α)
:
theorem
Function.IsFixedPt.birkhoffSum_eq
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
{f : α → α}
{x : α}
(h : IsFixedPt f x)
(g : α → M)
(n : ℕ)
:
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 : α)
:
theorem
birkhoffSum_apply_sub_birkhoffSum
{α : Type u_1}
{G : Type u_2}
[AddCommGroup G]
(f : α → α)
(g : α → G)
(n : ℕ)
(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.