English
Under Lipschitz and uniform continuity assumptions for f and g, the set of points x for which the Birkhoff average tends to l(x) is closed.
Русский
При условиях лиспшицевости f и равномерной непрерывности g множество точек x, для которых среднее Биркхоффа стремится к l(x), замкнуто.
LaTeX
$$$\\text{IsClosed}\\{x \\mid \\mathrm{Tendsto}(\\mathrm{birkhoffAverage} 𝕜 f g · x)\\;\\text{atTop}\\; (\\mathcal{N}(l x))\\}$$$
Lean4
/-- 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. -/
theorem isClosed_setOf_tendsto_birkhoffAverage (hf : LipschitzWith 1 f) (hg : UniformContinuous g) (hl : Continuous l) :
IsClosed {x | Tendsto (birkhoffAverage 𝕜 f g · x) atTop (𝓝 (l x))} :=
(uniformEquicontinuous_birkhoffAverage 𝕜 hf hg).equicontinuous.isClosed_setOf_tendsto hl
