Smooth functions are dense in W^{1,p}(Ω) (Meyers–Serrin)

For 1 ≤ p < ∞ and an arbitrary open set Ω of a finite-dimensional real inner product space, the elements of W^{1,p}(Ω) with a representative which is smooth on Ω are dense in W^{1,p}(Ω), in the full Sobolev norm. In other words H = W: the closure of C^∞(Ω) ∩ W^{1,p}(Ω) is all of W^{1,p}(Ω). No boundedness and no regularity of the boundary of Ω is assumed.

The approximants are smooth on Ω but need not be smooth up to its boundary, nor compactly supported in Ω: on standard nontrivial bounded domains (for example, Euclidean balls in positive dimension), W^{1,p}_0(Ω) is a proper subspace, so test functions are not dense. On the whole space, density of globally smooth representatives at every order is TauCeti.Wkp.dense_contDiff_representatives.

The argument

Take a decomposition of unity (ζ j) of Ω by test functions, together with cutoffs χ j equal to one on the support of ζ j and locally finite in Ω (IsOpen.exists_contDiff_decomposition_cutoff). Each piece ζ j u is compactly supported in Ω, so it lies in W^{1,p}_0(Ω) (TauCeti.W1p.contDiffSMul_mem_w1p0Submodule_of_hasCompactSupport) and is approximated by a test function ψ j to within ε 2^{-j}; cutting off, χ j ψ j still approximates ζ j u = χ j ζ j u, and now has support where χ j does. The sum f = ∑ j, χ j ψ j is locally finite in Ω, hence smooth there.

The series ∑ j, ζ j u need not converge to u in W^{1,p}(Ω): its partial sums are cutoffs of u, and those converge to u only for u ∈ W^{1,p}_0(Ω). So the comparison with u is made through the corrections instead. These are absolutely summable in the Banach space W^{1,p}(Ω), to some w of norm at most ε / 2; after passing to a subsequence, representatives of their partial sums converge almost everywhere on Ω to f - u. Hence u + w is within ε of u, and its value is represented by f.

Main declarations

• TauCeti.W1p.exists_contDiffOn_approximation: every u ∈ W^{1,p}(Ω) is a Sobolev-norm limit of elements with representatives smooth on Ω.
• TauCeti.W1p.dense_contDiffOn_representatives: those elements are dense in W^{1,p}(Ω).

References

• N. G. Meyers, J. Serrin, H = W, Proc. Nat. Acad. Sci. U.S.A. 51 (1964), 1055–1056.
• L. C. Evans, Partial Differential Equations, §5.3.2, Theorem 2.

theorem TauCeti.W1p.exists_contDiffOn_approximation {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)] (hp : p ≠ ⊤) (u : ↥(W1p mu Omega p)) : ∃ (v : ℕ → ↥(W1p mu Omega p)) (f : ℕ → E → ℝ), (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f j) ↑Omega) ∧ (∀ (j : ℕ), ↑↑(value (v j)) =ᵐ[mu.restrict ↑Omega] f j) ∧ Filter.Tendsto v Filter.atTop (nhds u)

Meyers–Serrin approximation in W^{1,p}(Ω). For 1 ≤ p < ∞ and an arbitrary open set Ω, every u ∈ W^{1,p}(Ω) is a limit, in the full Sobolev norm, of elements whose values are represented by functions smooth on Ω. No boundedness or boundary regularity of Ω is assumed.

theorem TauCeti.W1p.dense_contDiffOn_representatives {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)] (hp : p ≠ ⊤) : Dense {u : ↥(W1p mu Omega p) | ∃ (f : E → ℝ), ContDiffOn ℝ (↑⊤) f ↑Omega ∧ ↑↑(value u) =ᵐ[mu.restrict ↑Omega] f}

Meyers–Serrin: H = W in W^{1,p}(Ω). For 1 ≤ p < ∞ and an arbitrary open set Ω, the elements of W^{1,p}(Ω) represented by functions smooth on Ω are dense in W^{1,p}(Ω), in the full Sobolev norm.