exists_contDiff_dist_le — Mathlib

English

Every uniformly continuous f admits a ContDiffG that is uniformly close to f with any prescribed tolerance.

Русский

Любая равномерно непрерывная функция f допускает континуально гладкую аппроксимацию g, ближайшую к f на любом заданном допуске.

LaTeX

$$$ \exists g: E \to F, ContDiff \mathbb{R} \infty g \land \forall a, \ dist(g(a), f(a)) < \varepsilon $$$

Lean4

theorem exists_contDiff_dist_le (hf : UniformContinuous f) (hε : 0 < ε) :
    ∃ g : E → F, ContDiff ℝ ∞ g ∧ ∀ a, dist (g a) (f a) < ε :=
  by
  rcases Metric.uniformContinuous_iff.mp hf (ε / 2) (half_pos hε) with ⟨δ, hδ, hfδ⟩
  rcases hf.continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le hδ with ⟨g, hgc, hg⟩
  exact ⟨g, hgc, fun a ↦ (hg a _ fun _ h ↦ (hfδ h).le).trans_lt (half_lt_self hε)⟩

Похожие утверждения