Documentation

Mathlib.Dynamics.BirkhoffSum.NormedSpace

Birkhoff average in a normed space #

In this file we prove some lemmas about the Birkhoff average (birkhoffAverage) of a function which takes values in a normed space over or .

At the time of writing, all lemmas in this file are motivated by the proof of the von Neumann Mean Ergodic Theorem, see LinearIsometry.tendsto_birkhoffAverage_orthogonalProjection.

theorem Function.IsFixedPt.tendsto_birkhoffAverage {α : Type u_1} {E : Type u_2} (R : Type u_3) [DivisionSemiring R] [CharZero R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {f : αα} {x : α} (h : Function.IsFixedPt f x) (g : αE) :
Filter.Tendsto (fun (x_1 : ) => birkhoffAverage R f g x_1 x) Filter.atTop (nhds (g x))

The Birkhoff averages of a function g over the orbit of a fixed point x of f tend to g x as N → ∞. In fact, they are equal to g x for all N ≠ 0, see Function.IsFixedPt.birkhoffAverage_eq.

TODO: add a version for a periodic orbit.

theorem dist_birkhoffSum_apply_birkhoffSum {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : αα) (g : αE) (n : ) (x : α) :
dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)
theorem dist_birkhoffSum_birkhoffSum_le {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : αα) (g : αE) (n : ) (x : α) (y : α) :
dist (birkhoffSum f g n x) (birkhoffSum f g n y) Finset.sum (Finset.range n) fun (k : ) => dist (g (f^[k] x)) (g (f^[k] y))
theorem dist_birkhoffAverage_birkhoffAverage {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (𝕜 : Type u_3) [IsROrC 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : αα) (g : αE) (n : ) (x : α) (y : α) :
dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) = dist (birkhoffSum f g n x) (birkhoffSum f g n y) / n
theorem dist_birkhoffAverage_birkhoffAverage_le {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (𝕜 : Type u_3) [IsROrC 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : αα) (g : αE) (n : ) (x : α) (y : α) :
dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) (Finset.sum (Finset.range n) fun (k : ) => dist (g (f^[k] x)) (g (f^[k] y))) / n
theorem dist_birkhoffAverage_apply_birkhoffAverage {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (𝕜 : Type u_3) [IsROrC 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : αα) (g : αE) (n : ) (x : α) :
dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / n
theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (𝕜 : Type u_3) [IsROrC 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] {f : αα} {g : αE} {x : α} (h : Bornology.IsBounded (Set.range fun (x_1 : ) => g (f^[x_1] x))) :
Filter.Tendsto (fun (n : ) => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (nhds 0)

If a function g is bounded along the positive orbit of x under f, then the difference between Birkhoff averages of g along the orbit of f x and along the orbit of x tends to zero.

See also tendsto_birkhoffAverage_apply_sub_birkhoffAverage'.

theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (𝕜 : Type u_3) [IsROrC 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] {g : αE} (h : Bornology.IsBounded (Set.range g)) (f : αα) (x : α) :
Filter.Tendsto (fun (n : ) => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (nhds 0)

If a function g is bounded, then the difference between Birkhoff averages of g along the orbit of f x and along the orbit of x tends to zero.

See also tendsto_birkhoffAverage_apply_sub_birkhoffAverage.

theorem uniformEquicontinuous_birkhoffAverage (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [PseudoEMetricSpace X] [IsROrC 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : XX} {g : XE} (hf : LipschitzWith 1 f) (hg : UniformContinuous g) :

If f is a non-strictly contracting map (i.e., it is Lipschitz with constant 1) and g is a uniformly continuous, then the Birkhoff averages of g along orbits of f is a uniformly equicontinuous family of functions.

theorem isClosed_setOf_tendsto_birkhoffAverage (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [PseudoEMetricSpace X] [IsROrC 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : XX} {g : XE} {l : XE} (hf : LipschitzWith 1 f) (hg : UniformContinuous g) (hl : Continuous l) :
IsClosed {x : X | Filter.Tendsto (fun (x_1 : ) => birkhoffAverage 𝕜 f g x_1 x) Filter.atTop (nhds (l x))}

If f : X → X is a non-strictly contracting map (i.e., it is Lipschitz with constant 1), g : X → E is a uniformly continuous, and l : X → E is a continuous function, then the set of points x such that the Birkhoff average of g along the orbit of x tends to l x is a closed set.