Smooth approximation with uniform control of derivatives

A compactly supported C^N function can be approximated by compactly supported smooth functions, uniformly in every derivative of order at most N. The supports of all the approximants lie in one compact subset of any prescribed open neighborhood of the original support. On a compact subset of an open domain the same conclusion holds for C^N data without a global support assumption.

In particular, for N = 2 this supplies smooth approximations of a twice continuously differentiable function with simultaneous control of its value, gradient and Hessian on a localized state region. No third derivative of the original function is required.

The construction combines normalized-bump uniform approximation with HasCompactSupport.iteratedFDeriv_convolution_right and the compactly supported extension ContDiffOn.exists_contDiff_eventuallyEq_on_isCompact.

References

• L. C. Evans, Partial Differential Equations, Appendix C.4 (mollifiers).

theorem HasCompactSupport.tendstoUniformly_iteratedFDeriv_normed_convolution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {N : ℕ∞} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hfc : HasCompactSupport f) (hf : ContDiff ℝ (↑N) f) {ι : Type u_3} {l : Filter ι} {ρ : ι → ContDiffBump 0} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) {k : ℕ} (hk : ↑k ≤ N) : TendstoUniformly (fun (i : ι) => iteratedFDeriv ℝ k (MeasureTheory.convolution ((ρ i).normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ)) (iteratedFDeriv ℝ k f) l

Shrinking normalized-bump mollifications of compactly supported C^N data converge uniformly in each derivative of order at most N.

theorem ContDiff.exists_contDiff_hasCompactSupport_tendstoUniformly_iteratedFDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (hfc : HasCompactSupport f) {U : Set E} (hU : IsOpen U) (hfU : tsupport f ⊆ U) : ∃ (g : ℕ → E → F) (K : Set E), IsCompact K ∧ K ⊆ U ∧ (∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n) ∧ tsupport (g n) ⊆ K) ∧ ∀ (k : ℕ), ↑k ≤ N → TendstoUniformly (fun (n : ℕ) => iteratedFDeriv ℝ k (g n)) (iteratedFDeriv ℝ k f) Filter.atTop

Compactly supported C^N data admit smooth approximants converging uniformly in all available derivatives, with a common compact support inside any prescribed open neighborhood of their support.

theorem ContDiffOn.exists_contDiff_hasCompactSupport_tendstoUniformlyOn_iteratedFDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {N : ℕ∞} {U K : Set E} (hf : ContDiffOn ℝ (↑N) f U) (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) : ∃ (g : ℕ → E → F) (L : Set E), IsCompact L ∧ L ⊆ U ∧ (∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n) ∧ tsupport (g n) ⊆ L) ∧ ∀ (k : ℕ), ↑k ≤ N → TendstoUniformlyOn (fun (n : ℕ) => iteratedFDeriv ℝ k (g n)) (iteratedFDeriv ℝ k f) Filter.atTop K

On a compact subset of an open domain, C^N data have smooth approximants converging uniformly in every derivative through order N. All approximants have support in one compact subset of the domain. The derivatives of the datum are ordinary, not within derivatives, since the datum is C^N on an open neighborhood.