Global approximation by functions smooth up to the boundary

On a bounded domain with C¹ boundary, a class with an Lᵖ weak gradient is the W^{1,p}(Ω) limit of smooth compactly supported functions on the whole space. Evans proves this by shifting the class into the domain near each boundary point, mollifying, and patching with a partition of unity, and Guo follows him. The extension operator makes the shift unnecessary: the class extends to a compactly supported class on ℝᵈ with a weak gradient there, the mollifications of the extension are smooth, compactly supported, and converge to it in Lᵖ(ℝᵈ) together with their gradients, and the extension agrees with the class on Ω. Restricting to Ω gives the theorem, with approximants that are restrictions of C_c^∞(ℝᵈ) functions, which is a stronger conclusion than membership of C^∞ up to the boundary.

The gradient of the approximant is identified with the mollified weak gradient of the extension by EllipticPdes.Embedding.partialD_convolution_eq_of_hasWeakGradOn, and the mollified weak gradient is read back against the class's own gradient by uniqueness of the weak gradient on the open set Ω.

Main declarations

• EllipticPdes.Extension.exists_smooth_tendsto_of_hasWeakGradOn: the theorem for a class and its gradient given as functions.
• EllipticPdes.Extension.hasWeakGradOn_of_mem_W12: an element of the graph space W12 Ω has its gradient coordinates as a weak gradient.
• EllipticPdes.Extension.exists_smooth_tendsto_of_mem_W12: the theorem at p = 2 for the graph space, which is density of the smooth functions in H¹(Ω).

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.3.3 Theorem 3 (p. 266); James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.1.3.

theorem EllipticPdes.Extension.exists_smooth_tendsto_of_hasWeakGradOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : HasC1Boundary Ω) {p : ℝ} (hp : 1 ≤ p) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hmu : MeasureTheory.MemLp u (ENNReal.ofReal p) (MeasureTheory.volume.restrict Ω)) (hmg : ∀ (k : Fin d), MeasureTheory.MemLp (g k) (ENNReal.ofReal p) (MeasureTheory.volume.restrict Ω)) (hwg : Embedding.HasWeakGradOn Ω u g) : ∃ (v : ℕ → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (v n)) ∧ (∀ (n : ℕ), HasCompactSupport (v n)) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (v n - u) (ENNReal.ofReal p) (MeasureTheory.volume.restrict Ω)) Filter.atTop (nhds 0) ∧ ∀ (k : Fin d), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Sobolev.partialD k (v n) - g k) (ENNReal.ofReal p) (MeasureTheory.volume.restrict Ω)) Filter.atTop (nhds 0)

Global approximation by functions smooth up to the boundary (Evans §5.3.3 Theorem 3 at order one, Guo Theorem III.1.3). On a bounded open domain with C¹ boundary, a class with an Lᵖ weak gradient on the domain, 1 ≤ p < ∞, is the limit in W^{1,p}(Ω) of smooth compactly supported functions on ℝᵈ: the functions converge to the class in Lᵖ(Ω) and their partial derivatives to the components of the weak gradient.

The graph space

theorem EllipticPdes.Extension.inner_L2D_eq_integral {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (f h : Sobolev.L2D Ω) : inner ℝ f h = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑h x

The real inner product of two L²(Ω) classes is the integral of their product over Ω.

theorem EllipticPdes.Extension.hasWeakGradOn_of_mem_W12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.W12 Ω) : Embedding.HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑(U.ofLp 0) x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => ↑↑(U.ofLp k.succ) x

Weak gradient of an element of the graph space. The constraint defining W12 Ω is integration by parts against every test function, read coordinate by coordinate: the function coordinate has the gradient coordinates as its weak gradient on Ω.

theorem EllipticPdes.Extension.exists_smooth_tendsto_of_mem_W12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : HasC1Boundary Ω) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.W12 Ω) : ∃ (v : ℕ → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (v n)) ∧ (∀ (n : ℕ), HasCompactSupport (v n)) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (v n - fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑(U.ofLp 0) x) 2 (MeasureTheory.volume.restrict Ω)) Filter.atTop (nhds 0) ∧ ∀ (k : Fin d), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Sobolev.partialD k (v n) - fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑(U.ofLp k.succ) x) 2 (MeasureTheory.volume.restrict Ω)) Filter.atTop (nhds 0)

Density of the smooth functions in H¹(Ω) (Evans §5.3.3 Theorem 3 at k = 1, p = 2). On a bounded open domain with C¹ boundary, every element of the graph space W12 Ω is the H¹(Ω) limit of smooth compactly supported functions on ℝᵈ: the functions converge to its function coordinate in L²(Ω), and their partial derivatives to its gradient coordinates.