Smooth density in whole-space Sobolev spaces

For 1 ≤ p < ∞, the elements of W^{k,p}(ℝⁿ) with a smooth representative are dense in the full Sobolev norm, at every natural order k. The ambient space can be any finite-dimensional real inner product space with an additive Haar measure.

The Sobolev mollifier averages translations of the entire weak-derivative graph. Its value is represented by the classical convolution with a smooth compactly supported kernel, even when the original function has no compact support. Thus its smoothness and its convergence hold simultaneously: the approximation controls every recorded weak derivative, rather than only the value in Lᵖ.

The approximating smooth functions need not have compact support. Density of test functions in the higher-order spaces and smooth density on arbitrary open domains are separate results.

Main declarations

• TauCeti.Wkp.exists_contDiff_ae_eq_value_normedBumpL: a smooth representative of each whole-space Sobolev mollification.
• TauCeti.Wkp.exists_contDiff_approximation: a sequence of smooth representatives whose Sobolev classes converge in the full graph norm.
• TauCeti.Wkp.dense_contDiff_representatives: smooth density in the whole-space Sobolev norm.

References

L. C. Evans, Partial Differential Equations, §5.3.1. The formal construction uses TauCeti.Wkp.normedBumpL and TauCeti.normedBumpLp_ae_eq_convolution, together with Mathlib's HasCompactSupport.contDiff_convolution_left.

theorem TauCeti.Wkp.instIsAddHaarMeasureRestrictCoeOpensTop_2 {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] : (mu.restrict ↑⊤).IsAddHaarMeasure

theorem TauCeti.Wkp.exists_contDiff_ae_eq_value_normedBumpL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (k : ℕ) (u : Wkp mu ⊤ p k) : ∃ (f : E → ℝ), ContDiff ℝ (↑⊤) f ∧ ↑↑(value k ((normedBumpL hp phi k) u)) =ᵐ[mu.restrict ↑⊤] f

Every whole-space Sobolev mollification has a smooth representative, without any compact-support assumption on the original function.

theorem TauCeti.Wkp.exists_contDiff_approximation {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (k : ℕ) (u : Wkp mu ⊤ p k) : ∃ (v : ℕ → Wkp mu ⊤ p k) (f : ℕ → E → ℝ), (∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) ∧ (∀ (j : ℕ), ↑↑(value k (v j)) =ᵐ[mu.restrict ↑⊤] f j) ∧ Filter.Tendsto v Filter.atTop (nhds u)

Every whole-space W^{k,p} element, for finite p, is a Sobolev-norm limit of elements with smooth representatives. No boundedness or support condition is imposed on the element.

theorem TauCeti.Wkp.dense_contDiff_representatives {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (k : ℕ) : Dense {u : Wkp mu ⊤ p k | ∃ (f : E → ℝ), ContDiff ℝ (↑⊤) f ∧ ↑↑(value k u) =ᵐ[mu.restrict ↑⊤] f}

Smooth representatives are dense in W^{k,p}(ℝⁿ) for 1 ≤ p < ∞, with density measured in the full Sobolev norm, including every recorded weak derivative.