Documentation

Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox

Density of smooth functions in the space of continuous functions #

In this file we prove that smooth functions are dense in the set of continuous functions from a real finite dimensional vector space to a Banach space, see ContinuousMap.dense_setOf_contDiff. We also prove several unbundled versions of this statement.

The heavy part of the proof is done upstream in ContDiffBump.dist_normed_convolution_le and HasCompactSupport.contDiff_convolution_left. Here we wrap these results removing measure-related arguments from the assumptions.

theorem MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {f : EF} {ε : } [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [μ.IsAddHaarMeasure] (hf : LocallyIntegrable f μ) ( : 0 < ε) :
∃ (g : EF), ContDiff (↑) g ∀ (a : E) (δ : ), (∀ xMetric.ball a ε, dist (f x) (f a) δ)dist (g a) (f a) δ
theorem Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {f : EF} {ε : } (hf : Continuous f) ( : 0 < ε) :
∃ (g : EF), ContDiff (↑) g ∀ (a : E) (δ : ), (∀ xMetric.ball a ε, dist (f x) (f a) δ)dist (g a) (f a) δ
theorem UniformContinuous.exists_contDiff_dist_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] [NormedAddCommGroup F] [NormedSpace F] [CompleteSpace F] {f : EF} {ε : } (hf : UniformContinuous f) ( : 0 < ε) :
∃ (g : EF), ContDiff (↑) g ∀ (a : E), dist (g a) (f a) < ε

Infinitely smooth functions are dense in the space of continuous functions.