exists_contDiff_dist_le_of_forall_mem_ball_dist_le

English

For LocallyIntegrable f with small ball distance control, there exists a ContDiff function g approximating f on balls, with uniform control on distortions.

Русский

Для LocallyIntegrable f сохраняется аппроксимация континно гладкой функцией g на шаре с контролируемым отклонением.

LaTeX

$$$ \exists g: E \to F, \ ContDiff \mathbb{R} \infty g \land \forall a, \forall \delta, (\forall x \in \mathrm{ball}(a,\varepsilon), \|f(x)-f(a)\| \le \delta) \Rightarrow \|g(a)-f(a)\| \le \delta $$$

Lean4

theorem exists_contDiff_dist_le_of_forall_mem_ball_dist_le (hf : Continuous f) (hε : 0 < ε) :
    ∃ g : E → F, ContDiff ℝ ∞ g ∧ ∀ a, ∀ δ, (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ :=
  by
  borelize E
  exact (hf.locallyIntegrable (μ := .addHaar)).exists_contDiff_dist_le_of_forall_mem_ball_dist_le hε

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