Test functions are dense in whole-space higher-order Sobolev spaces

For 1 ≤ p < ∞, test functions are dense in W^{k,p}(E) for every natural order k, where E is a finite-dimensional real inner product space equipped with an additive Haar measure. Thus W^{k,p}_0(E) = W^{k,p}(E) in the full iterated graph norm.

Smooth Sobolev representatives are already dense by mollification. Expanding smooth cutoffs approximate each such representative simultaneously in every classical derivative through order k. Identification with the recorded weak derivatives then upgrades this convergence to the bundled Sobolev norm. No boundary regularity or boundedness assumption is needed because this is a whole-space result; it does not assert test-function density on proper open domains.

The argument follows Evans, Partial Differential Equations, §5.3.1, using TauCeti.exists_contDiff_hasCompactSupport_approximation and TauCeti.Wkp.dense_contDiff_representatives.

theorem TauCeti.Wkp.tendsto_ofTestFunctionₗ_of_contDiffOn {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {I : Type u_2} {l : Filter I} (k : ℕ) (u : Wkp mu Omega p k) {f : E → ℝ} (hf : ContDiffOn ℝ (↑k) f ↑Omega) (hu : ↑↑(value k u) =ᵐ[mu.restrict ↑Omega] f) (phi : I → TestFunction Omega ℝ ⊤) (hphi : ∀ i ≤ k, Filter.Tendsto (fun (j : I) => MeasureTheory.eLpNorm (iteratedFDeriv ℝ i ⇑(phi j) - iteratedFDeriv ℝ i f) p (mu.restrict ↑Omega)) l (nhds 0)) : Filter.Tendsto (fun (j : I) => (ofTestFunctionₗ k) (phi j)) l (nhds u)

Simultaneous Lᵖ convergence of the classical derivatives of test functions through order k implies convergence in the full W^{k,p} norm to a Sobolev representative that is C^k on the domain. This implication works on any open domain, not only on the whole space.

theorem TauCeti.wkp0Submodule_top_eq_top {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 : ℕ) : wkp0Submodule mu ⊤ p k = ⊤

W^{k,p}_0(E) = W^{k,p}(E), as an equality of closed subspaces of the whole-space Sobolev space, for every natural order and 1 ≤ p < ∞.

theorem TauCeti.Wkp.denseRange_ofTestFunctionₗ_top {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 : ℕ) : DenseRange ⇑(ofTestFunctionₗ k)

Test functions are dense in the full whole-space W^{k,p} norm for 1 ≤ p < ∞.