Mollification of compactly supported higher-order Sobolev functions

The first-order part of a W^{k+1,p} function records its value and weak gradient. If the value vanishes almost everywhere outside a compact set, the gradient vanishes there too, since the complement is open. A smooth mollification is then a test function. The resulting equality holds in the full W^{k+1,p} space: uniqueness of weak derivatives determines all its higher components from its value.

This supplies the compact-support step in the density of test functions in whole-space Sobolev spaces. The remaining step is to approximate arbitrary higher-order Sobolev functions by compactly supported ones.

The mollification argument follows Evans, Partial Differential Equations, §5.3.1.

theorem TauCeti.Wkp.firstOrder_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 + 1)) : firstOrder k ((normedBumpL hp phi (k + 1)) u) = (W1p.normedBumpL hp phi) (firstOrder k u)

First-order projection commutes with whole-space mollification.

theorem TauCeti.Wkp.normedBumpL_mem_range_of_ae_eq_zero {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 + 1)) {K : Set E} (hK : IsCompact K) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑⊤, x ∉ K → ↑↑↑(firstOrder k u) x = 0) : (normedBumpL hp phi (k + 1)) u ∈ (ofTestFunctionₗ (k + 1)).range

Mollification of a higher-order Sobolev function whose first-order jet has compact support is the image of a smooth compactly supported test function.

theorem TauCeti.Wkp.mem_wkp0Submodule_top_of_firstOrder_ae_eq_zero {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 + 1)) {K : Set E} (hK : IsCompact K) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑⊤, x ∉ K → ↑↑↑(firstOrder k u) x = 0) : u ∈ wkp0Submodule mu ⊤ p (k + 1)

A whole-space higher-order Sobolev function whose first-order jet vanishes outside a compact set belongs to the closure of test functions in the full higher-order norm.

theorem TauCeti.Wkp.firstOrder_ae_eq_zero_of_value_ae_eq_zero {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)] (k : ℕ) (u : Wkp mu Omega p (k + 1)) {V : TopologicalSpace.Opens E} (hV : V ≤ Omega) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑V, ↑↑(value (k + 1) u) x = 0) : ∀ᵐ (x : E) ∂mu.restrict ↑V, ↑↑↑(firstOrder k u) x = 0

If the value vanishes almost everywhere on an open subset, so does its first-order jet.

theorem TauCeti.Wkp.normedBumpL_mem_range_of_value_ae_eq_zero {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 + 1)) {K : Set E} (hK : IsCompact K) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑⊤, x ∉ K → ↑↑(value (k + 1) u) x = 0) : (normedBumpL hp phi (k + 1)) u ∈ (ofTestFunctionₗ (k + 1)).range

Mollifying a higher-order Sobolev function supported in a compact set produces a test function representing the same higher-order Sobolev element.

theorem TauCeti.Wkp.mem_wkp0Submodule_top_of_value_ae_eq_zero {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 + 1)) {K : Set E} (hK : IsCompact K) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑⊤, x ∉ K → ↑↑(value (k + 1) u) x = 0) : u ∈ wkp0Submodule mu ⊤ p (k + 1)

A compactly supported whole-space higher-order Sobolev function belongs to the closure of test functions in the full higher-order norm.