Local smooth approximation in higher-order Sobolev spaces

On an open subdomain with compact closure inside Ω, restrictions of test functions on Ω approximate every W^{k,p}(Ω) function in the full Sobolev norm, for 1 ≤ p < ∞. No regularity of the boundary is needed. The approximants control every weak derivative through order k, and are smooth on the entire larger domain. This is the local approximation step in the Meyers–Serrin theorem; it does not assert global density on an arbitrary open domain.

The construction mollifies zero extensions at radii smaller than the distance to the boundary, then multiplies the smooth representative by a fixed test function equal to one near the smaller domain. Interior derivative identities identify all its derivatives with mollified weak derivative fields.

References

L. C. Evans, Partial Differential Equations, Chapter 5, §5.3.1. The proof uses the interior convolution identities and the local Lᵖ approximate identity already in Tau Ceti.

theorem TauCeti.Wkp.instIsAddHaarMeasureRestrictUniv {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] : (mu.restrict Set.univ).IsAddHaarMeasure

theorem TauCeti.Wkp.exists_testFunction_approximation_restrictL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hcompact : IsCompact (closure ↑U)) (hclosure : closure ↑U ⊆ ↑Omega) (k : ℕ) (u : Wkp mu Omega p k) : ∃ (psi : ℕ → TestFunction Omega ℝ ⊤), Filter.Tendsto (fun (j : ℕ) => (restrictL ⋯ k) ((ofTestFunctionₗ k) (psi j))) Filter.atTop (nhds ((restrictL ⋯ k) u))

On every open subdomain with compact closure inside Ω, restrictions of test functions on Ω approximate the restriction of a W^{k,p}(Ω) element in the full Sobolev norm. The order is arbitrary, and no boundary regularity is assumed.

theorem TauCeti.Wkp.restrictL_mem_closure_range_ofTestFunctionₗ {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hcompact : IsCompact (closure ↑U)) (hclosure : closure ↑U ⊆ ↑Omega) (k : ℕ) (u : Wkp mu Omega p k) : (restrictL ⋯ k) u ∈ closure (Set.range fun (psi : TestFunction Omega ℝ ⊤) => (restrictL ⋯ k) ((ofTestFunctionₗ k) psi))

The restriction of a W^{k,p}(Ω) function to an open subdomain compactly contained in Ω is in the Sobolev-norm closure of restrictions of test functions on the larger domain.

theorem TauCeti.W1p.restrictL_mem_closure_range_ofTestFunctionₗ {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hcompact : IsCompact (closure ↑U)) (hclosure : closure ↑U ⊆ ↑Omega) (u : ↥(W1p mu Omega p)) : (restrictL ⋯) u ∈ closure (Set.range fun (psi : TestFunction Omega ℝ ⊤) => (restrictL ⋯) ((ofTestFunctionₗ mu Omega p) psi))

The order-one case of TauCeti.Wkp.restrictL_mem_closure_range_ofTestFunctionₗ, stated with W1p.restrictL and W1p.ofTestFunctionₗ so that first-order callers need not rewrite through Wkp.restrictL_one and Wkp.ofTestFunctionₗ_one.