Theorems · Theorem · dynamical systems

uniformEquicontinuous_birkhoffAverage

∀ (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : RCLike 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : X → X} {g : X → E},
  LipschitzWith 1 f → 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.

Defined in

Mathlib.Dynamics.BirkhoffSum.NormedSpace

Cited by

1 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpaceRCLikeNormedAddCommGroupNormedSpace