English
If g is bounded, then for all f, x, the same Tendsto result holds without the extra hypothesis, i.e., Tendsto (birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0).
Русский
Если g ограничен, то предел той же разности между средними Биркхоффа существует и равен нулю.
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,
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' {g : α → E} (h : Bornology.IsBounded (range g)) (f : α → α)
(x : α) : Tendsto (fun n ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0) :=
tendsto_birkhoffAverage_apply_sub_birkhoffAverage _ <| h.subset <| range_comp_subset_range _ _
