Uniform approximation of continuous and C¹ functions by test functions

Let Ω be an open set of a finite-dimensional real normed space E. Mollifying a continuous function supported in a compact set K by normalized bumps of small radius gives test functions on Ω supported in a fixed closed thickening of K that converge to it uniformly, as long as that thickening lies in Ω. For a C¹ function the derivatives of the mollifications are the mollifications of its derivative (Mathlib's HasCompactSupport.hasFDerivAt_convolution_right), so they converge uniformly as well. The construction follows Mathlib's MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le and UniformContinuous.exists_contDiff_dist_le (in Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox), with added control of the support; the error estimate is Mathlib's ContDiffBump.dist_normed_convolution_le.

Main results

• Continuous.exists_testFunction_dist_le: a continuous function supported in a compact set K is uniformly approximated by test functions supported in any closed thickening of K that lies in Ω.
• ContDiff.exists_testFunction_dist_le_and_dist_fderiv_le: a C¹ function supported in a compact set K is approximated in the same way, uniformly together with its derivative.

References

• L. Hörmander, The Analysis of Linear Partial Differential Operators I, Chapter I (regularization by convolution).

theorem Continuous.exists_testFunction_dist_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : Continuous f) {K : Set E} (hK : IsCompact K) (hfK : tsupport f ⊆ K) {δ : ℝ} (hδ : 0 < δ) (hKΩ : Metric.cthickening δ K ⊆ ↑Ω) {ε : ℝ} (hε : 0 < ε) : ∃ (φ : TestFunction Ω F ⊤), tsupport ⇑φ ⊆ Metric.cthickening δ K ∧ ∀ (x : E), dist (φ x) (f x) ≤ ε

A continuous function supported in a compact set K is uniformly approximated by test functions on Ω, as long as a closed thickening cthickening δ K lies in Ω: for every ε > 0 there is a test function on Ω, supported in cthickening δ K, within ε of f everywhere.

theorem ContDiff.exists_testFunction_dist_le_and_dist_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : ContDiff ℝ 1 f) {K : Set E} (hK : IsCompact K) (hfK : tsupport f ⊆ K) {δ : ℝ} (hδ : 0 < δ) (hKΩ : Metric.cthickening δ K ⊆ ↑Ω) {ε : ℝ} (hε : 0 < ε) : ∃ (φ : TestFunction Ω F ⊤), tsupport ⇑φ ⊆ Metric.cthickening δ K ∧ ∀ (x : E), Dist.dist (φ x) (f x) ≤ ε ∧ Dist.dist (fderiv ℝ (⇑φ) x) (fderiv ℝ f x) ≤ ε

A C¹ function supported in a compact set K is approximated by test functions on Ω uniformly together with its derivative, as long as a closed thickening cthickening δ K lies in Ω: for every ε > 0 there is a test function on Ω, supported in cthickening δ K, within ε of f everywhere and whose derivative is within ε of fderiv ℝ f everywhere.