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) [RCLike 𝕜] [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) [RCLike 𝕜] [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) [RCLike 𝕜] [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) [RCLike 𝕜] [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) [RCLike 𝕜] [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] [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : X → X} {g : X → E} (hf : LipschitzWith 1 f) (hg : UniformContinuous g) : UniformEquicontinuous (birkhoffAverage 𝕜 f 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] [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : X → X} {g : X → E} {l : X → E} (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.