Theorems · Theorem · dynamical systems

isClosed_setOfPred_tendsto_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 l : X → E},
  LipschitzWith 1 f →
    UniformContinuous g →
      Continuous l → IsClosed {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.

Defined in

Mathlib.Dynamics.BirkhoffSum.NormedSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceRCLikeNormedAddCommGroupNormedSpace