Convergence of interior mollifications of Sobolev derivative fields

The value and every recorded weak derivative of a domain Sobolev function are Lᵖ classes. Extend each field by zero, mollify it on the ambient space, and restrict back to an open subdomain. For finite p, these fields converge in the local Lᵖ norm as the bump radius tends to zero. This is the norm-convergence input for constructing local smooth Sobolev approximations; the derivative identities for the mollifications are separate.

References

L. C. Evans, Partial Differential Equations, Chapter 5, §5.3.1.

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

theorem TauCeti.Wkp.tendsto_mollified_value {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 ≠ ⊤) (hU : U ≤ Omega) {I : Type u_2} {l : Filter I} {phi : I → ContDiffBump 0} (hphi : Filter.Tendsto (fun (i : I) => (phi i).rOut) l (nhds 0)) (k : ℕ) (u : Wkp mu Omega p k) : Filter.Tendsto (fun (i : I) => (MeasureTheory.Lp.LpToLpOfMeasureLeSMul tendsto_mollified_value._proof_1 ⋯) ((normedBumpLp hp (phi i) (mu.restrict Set.univ)) ((extendByZeroLpₗᵢ ℝ mu ⋯ ⋯) (value k u)))) l (nhds (value k ((restrictL hU k) u)))

Mollification of the zero extension of the value of u ∈ W^{k,p}(Ω) converges in Lᵖ(U) to the value of the restriction, for every open U ⊆ Ω and p < ∞.

theorem TauCeti.Wkp.tendsto_mollified_iteratedGradient {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 ≠ ⊤) (hU : U ≤ Omega) {I : Type u_2} {l : Filter I} {phi : I → ContDiffBump 0} (hphi : Filter.Tendsto (fun (i : I) => (phi i).rOut) l (nhds 0)) (k : ℕ) (u : Wkp mu Omega p (k + 1)) : Filter.Tendsto (fun (i : I) => (MeasureTheory.Lp.LpToLpOfMeasureLeSMul tendsto_mollified_value._proof_1 ⋯) ((normedBumpLp hp (phi i) (mu.restrict Set.univ)) ((extendByZeroLpₗᵢ ℝ mu ⋯ ⋯) (iteratedGradient k u)))) l (nhds (iteratedGradient k ((restrictL hU (k + 1)) u)))

Mollification of the zero extension of the highest derivative of u ∈ W^{k+1,p}(Ω) converges in Lᵖ(U) to the corresponding derivative of its restriction. Together with the value case, this controls every component of the iterated graph norm.