Approximation of continuous functions by smooth functions

In this file, we deduce from the existence of smooth partitions of unity that any continuous map from a real σ-compact finite dimensional manifold M to a real normed space F can be approximated uniformly by smooth functions.

More precisely, we strengthen this result in three ways :

• instead of a single number ε > 0, one may prescribe the precision of the approximation using an arbitrary continuous positive function ε : M → ℝ. This allows, for example, a control on the asymptotic behaviour of the approximation (e.g, choosing a precision ε which vanishes at infinity yields that continuous functions vanishing at infinity can be approximated by smooth functions vanishing at infinity).
• if the original map f already has the desired regularity on some neighborhood of a closed set M, one can choose an approximation which stays equal to f on S. This allows for some additional control in a setting with iterated approximations.
• finally, one may prescribe the approximation to vanish wherever the original function vanishes. For example, this shows that continuous functions supported on some compact set K may be approximated uniformly by smooth function supported on the same compact K. (Compare with arguments based on convolution where one needs to thicken K a bit).

Main results

• Continuous.exists_contMDiff_approx_and_eqOn: approximating a continuous function f : M → F by a C^n function g : M → E, with precision prescribed by a continuous positive ε : M → ℝ, while ensuring that support g ⊆ support f and that g coincides with f on some closed set S in the neighborhood of which f is already C^n.
• Continuous.exists_contMDiff_approx: a simpler version of the previous result when one does not care about prescribing points with g x = f x. One still gets support g ⊆ support f for free, so we put it in the conclusion.
• Continuous.exists_contDiff_approx_and_eqOn, Continuous.exists_contDiff_approx: specializations of the previous results when M = E is a normed space.

Implementation notes

With minor work, we could strenghten the statements in the following ways:

• the precision function ε : M → ℝ may be assumed LowerSemicontinuous instead of Continuous,
• the condition support g ⊆ support f, which translates to ∀ x, f x = 0 → g x = 0, may be strenghtened to ∀ x, f x = h x → g x = h x for some arbitrary smooth h : M → F.

This file depends on the manifold library, which may be annoying if you only need the normed space statements. Please do not let this refrain you from using them if they apply naturally in your context: if this is too much of a problem, you should complain on Zulip, so that we get more data about the need for a non-manifold version of SmoothPartitionOfUnity.

TODO

• More generally, all results should apply to approximating continuous sections of a smooth vector bundle by smooth sections.
• If needed, specialize to M = U an open subset of a normed space E (we currently do M = E only).

theorem Continuous.exists_contMDiff_approx_and_eqOn {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] [T2Space M] {f : M → F} {ε : M → ℝ} (n : ℕ∞) (f_cont : Continuous f) (ε_cont : Continuous ε) (ε_pos : ∀ (x : M), 0 < ε x) {S U : Set M} (hS : IsClosed S) (hU : U ∈ nhdsSet S) (hfU : ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) f U) : ∃ (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑n), (∀ (x : M), dist (g x) (f x) < ε x) ∧ Set.EqOn (⇑g) f S ∧ Function.support ⇑g ⊆ Function.support f

theorem Continuous.exists_contMDiff_approx {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] [T2Space M] {f : M → F} {ε : M → ℝ} (n : ℕ∞) (f_cont : Continuous f) (ε_cont : Continuous ε) (ε_pos : ∀ (x : M), 0 < ε x) : ∃ (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑n), (∀ (x : M), dist (g x) (f x) < ε x) ∧ Function.support ⇑g ⊆ Function.support f

theorem Continuous.exists_contDiff_approx_and_eqOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {ε : E → ℝ} (n : ℕ∞) (f_cont : Continuous f) (ε_cont : Continuous ε) (ε_pos : ∀ (x : E), 0 < ε x) {S U : Set E} (hS : IsClosed S) (hU : U ∈ nhdsSet S) (hfU : ContDiffOn ℝ (↑n) f U) : ∃ (g : E → F), ContDiff ℝ (↑n) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ Set.EqOn g f S ∧ Function.support g ⊆ Function.support f

theorem Continuous.exists_contDiff_approx {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {ε : E → ℝ} (n : ℕ∞) (f_cont : Continuous f) (ε_cont : Continuous ε) (ε_pos : ∀ (x : E), 0 < ε x) : ∃ (g : E → F), ContDiff ℝ (↑n) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ Function.support g ⊆ Function.support f