Test functions are dense in W^{1,p}(ℝⁿ)

For 1 ≤ p < ∞, every function in the whole-space Sobolev space W^{1,p}(ℝⁿ) is a W^{1,p}-limit of test functions:

W^{1,p}_0(ℝⁿ) = W^{1,p}(ℝⁿ).

The ambient space is any finite-dimensional real inner product space E with an additive Haar measure; ℝⁿ stands for the whole-space case Ω = ⊤ below. For a nonempty bounded domain in a space of positive dimension the two spaces differ, since the Poincaré inequality excludes the nonzero constants from W^{1,p}_0(Ω); so the statement is genuinely about the whole space.

Density of test functions

The mollification operator TauCeti.W1p.normedBumpL on W^{1,p}(ℝⁿ) converges to the identity (TauCeti.W1p.tendsto_normedBumpL). If the jet of u vanishes outside a compact set, its mollification is a test function (TauCeti.W1p.normedBumpL_mem_range_of_ae_eq_zero). A general u is first truncated by the rescaled bumps ψ(x / R): the Leibniz rule of TauCeti.W1p.contDiffSMul computes the truncated jet, which agrees with the jet of u on the ball of radius R and is dominated by a fixed multiple of it, so the truncations converge to u by dominated convergence. Closedness of W^{1,p}_0(ℝⁿ) then gives the theorem.

Main declarations

• TauCeti.W1p.mem_w1p0Submodule_top: every u ∈ W^{1,p}(ℝⁿ) lies in W^{1,p}_0(ℝⁿ).
• TauCeti.w1p0Submodule_top_eq_top: W^{1,p}_0(ℝⁿ) = W^{1,p}(ℝⁿ) for p < ∞.
• TauCeti.W1p.denseRange_ofTestFunctionₗ_top: test functions are dense in W^{1,p}(ℝⁿ).

References

L. C. Evans, Partial Differential Equations, §5.3.1; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 9.2.

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

The whole-space restriction of an additive Haar measure is the measure itself.

Truncation

Density

theorem TauCeti.W1p.mem_w1p0Submodule_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 ≠ ⊤) (u : ↥(W1p mu ⊤ p)) : u ∈ w1p0Submodule mu ⊤ p

Every function in W^{1,p}(ℝⁿ) is a limit of test functions, for 1 ≤ p < ∞. Truncate by rescaled cutoffs, then mollify the compactly supported truncations.

theorem TauCeti.w1p0Submodule_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 ≠ ⊤) : w1p0Submodule mu ⊤ p = ⊤

W^{1,p}_0(ℝⁿ) = W^{1,p}(ℝⁿ) for 1 ≤ p < ∞: on the whole space the zero-boundary condition is no condition at all. Both restrictions are needed when E has positive dimension: there the analogous equality fails for a nonempty bounded domain, and it fails for p = ∞, where the constant 1 is not a limit of test functions.

theorem TauCeti.W1p.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 ≠ ⊤) : DenseRange ⇑(ofTestFunctionₗ mu ⊤ p)

Test functions are dense in W^{1,p}(ℝⁿ) for 1 ≤ p < ∞.