Theorems · Theorem · dynamical systems

tendsto_birkhoffAverage_apply_sub_birkhoffAverage

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

Defined in

Mathlib.Dynamics.BirkhoffSum.NormedSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeNormedSpace