English
If f is Lipschitz with constant 1 and g is uniformly continuous, then the family {birkhoffAverage 𝕜 f g} is uniformly equicontinuous as a family of functions.
Русский
Если f является Липшицевой с константой 1, а g равномерно непрерывна, то Familiey {birkhoffAverage 𝕜 f g} тождественно равномерно равноочно непрерывна.
LaTeX
$$$\\mathrm{UniformEquicontinuous}(\\lambda n. \\mathrm{birkhoffAverage} 𝕜 f g n)$$$
Lean4
/-- 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. -/
theorem uniformEquicontinuous_birkhoffAverage (hf : LipschitzWith 1 f) (hg : UniformContinuous g) :
UniformEquicontinuous (birkhoffAverage 𝕜 f g) :=
by
refine Metric.uniformity_basis_dist_le.uniformEquicontinuous_iff_right.2 fun ε hε ↦ ?_
rcases (uniformity_basis_edist_le.uniformContinuous_iff Metric.uniformity_basis_dist_le).1 hg ε hε with ⟨δ, hδ₀, hδε⟩
refine mem_uniformity_edist.2 ⟨δ, hδ₀, fun {x y} h n ↦ ?_⟩
calc
dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) ≤
(∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
dist_birkhoffAverage_birkhoffAverage_le ..
_ ≤ (∑ _k ∈ Finset.range n, ε) / n := by
gcongr
refine hδε _ _ ?_
simpa using (hf.iterate _).edist_le_mul_of_le h.le
_ = n * ε / n := by simp
_ ≤ ε := by rcases eq_or_ne n 0 with hn | hn <;> simp [hn, hε.le, mul_div_cancel_left₀]
