# 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`

.

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.

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'`

.

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.

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.

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.