English
A Hölder continuous map on a subset with positive exponent is uniformly continuous on that subset.
Русский
Пусть отображение Хёльдера на подмножестве с положительным показателем; тогда оно равномерно непрерывно на этом подмножестве.
LaTeX
$$$\\text{HolderOnWith } C r f s \\Rightarrow 0 < r \\Rightarrow \\text{UniformContinuousOn } f s$$$
Lean4
/-- A Hölder continuous function is uniformly continuous -/
protected theorem uniformContinuousOn (hf : HolderOnWith C r f s) (h0 : 0 < r) : UniformContinuousOn f s :=
by
refine EMetric.uniformContinuousOn_iff.2 fun ε εpos => ?_
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top h0
rcases ENNReal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩
exact ⟨δ, δ0, fun hx y hy h => (hf.edist_le hx hy).trans_lt (H h)⟩
