English
If g is bounded along the range of f^·x, then the difference between the n-th Birkhoff averages at f x and x tends to zero: Tendsto (λn, birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0).
Русский
Если значения g ограничены на диапазоне орбит, то разность между n-й средней Биркхоффа на f x и на x стремится к нулю.
LaTeX
$$$\\operatorname{Tendsto}\\Big(\\lambda n. \\mathrm{birkhoffAverage}(𝕜,f,g,n,(f x)) - \\mathrm{birkhoffAverage}(𝕜,f,g,n,x)\\Big)\\;\\text{atTop}\\; (\\mathcal{N}(0))$$$
Lean4
/-- 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'`. -/
theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage {f : α → α} {g : α → E} {x : α}
(h : Bornology.IsBounded (range (g <| f^[·] x))) :
Tendsto (fun n ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0) :=
by
rcases Metric.isBounded_range_iff.1 h with ⟨C, hC⟩
have : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop
refine squeeze_zero_norm (fun n ↦ ?_) this
rw [← dist_eq_norm, dist_birkhoffAverage_apply_birkhoffAverage]
gcongr
exact hC n 0
