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 : E → F}
{ε : ℝ}
[MeasurableSpace E]
[BorelSpace E]
{μ : Measure E}
[μ.IsAddHaarMeasure]
(hf : LocallyIntegrable f μ)
(hε : 0 < ε)
:
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 : E → F}
{ε : ℝ}
(hf : Continuous f)
(hε : 0 < ε)
:
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 : E → F}
{ε : ℝ}
(hf : UniformContinuous f)
(hε : 0 < ε)
:
theorem
ContinuousMap.dense_setOf_contDiff
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
:
Infinitely smooth functions are dense in the space of continuous functions.