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_setOfPred_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 < ε) : ∃ (g : E → F), ContDiff ℝ (↑⊤) g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ Metric.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 : E → F} {ε : ℝ} (hf : Continuous f) (hε : 0 < ε) : ∃ (g : E → F), ContDiff ℝ (↑⊤) g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ Metric.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 : E → F} {ε : ℝ} (hf : UniformContinuous f) (hε : 0 < ε) : ∃ (g : E → F), ContDiff ℝ (↑⊤) g ∧ ∀ (a : E), dist (g a) (f a) < ε

theorem ContinuousMap.dense_setOfPred_contDiff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] : Dense {f : C(E, F) | ContDiff ℝ ↑⊤ ⇑f}

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

@[deprecated ContinuousMap.dense_setOfPred_contDiff (since := "2026-07-09")]

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] : Dense {f : C(E, F) | ContDiff ℝ ↑⊤ ⇑f}

Alias of ContinuousMap.dense_setOfPred_contDiff.

---

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