Extension operator between the graph spaces

EllipticPdes.Extension.exists_extLinear is the extension operator on pairs of a class and its gradient, given as functions. Guo's Theorem III.2.2 states it as a bounded linear map E : W^{1,p}(Ω) → W^{1,p}(ℝⁿ) between the Sobolev spaces. This file states it that way at p = 2, between the graph spaces W12 Ω and W12 ℝᵈ of this development.

The passage from functions to classes needs nothing beyond the bound. A linear map on representatives whose image is bounded in L²(ℝᵈ) by the L²(Ω) seminorms of the input descends to classes: two representatives of one class differ by a pair of seminorm zero, so their images differ by a function of seminorm zero, which vanishes almost everywhere. The map is then linear on the classes, bounded by the same constant, its image lies in the graph space of the whole space because the image pair has a weak gradient there, and the three clauses of the theorem are read off exists_extLinear through the representatives.

Main declarations

• EllipticPdes.Extension.mem_W12_of_hasWeakGradOn: a class with an L² weak gradient, paired with it, lies in the graph space.
• EllipticPdes.Extension.exists_extW12: the extension operator as a bounded linear map between the graph spaces, with the three clauses of Guo III.2.2.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20); L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1 (p. 253).

theorem EllipticPdes.Extension.ae_of_ae_restrict_univ {d : ℕ} {p : EuclideanSpace ℝ (Fin d) → Prop} (h : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Set.univ, p x) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), p x

Almost everywhere for the restriction to the whole space is almost everywhere.

Membership of a pair in the graph space

theorem EllipticPdes.Extension.mem_W12_of_hasWeakGradOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {F : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict Ω)) (hG : ∀ (k : Fin d), MeasureTheory.MemLp (G k) 2 (MeasureTheory.volume.restrict Ω)) (hwg : Embedding.HasWeakGradOn Ω F G) : WithLp.toLp 2 (Fin.cons (MeasureTheory.MemLp.toLp F hF) fun (k : Fin d) => MeasureTheory.MemLp.toLp (G k) ⋯) ∈ Sobolev.W12 Ω

Membership of a class with an L² weak gradient in the graph space, paired with that gradient. This is the converse of hasWeakGradOn_of_mem_W12: the constraint defining W12 Ω is the integration by parts the weak gradient asserts.

The operator on the graph spaces

theorem EllipticPdes.Extension.exists_extW12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : HasC1Boundary Ω) {Ω' : Set (EuclideanSpace ℝ (Fin d))} (hΩ'open : IsOpen Ω') (hsub : closure Ω ⊆ Ω') : ∃ (E : ↥(Sobolev.W12 Ω) →L[ℝ] ↥(Sobolev.W12 Set.univ)) (C : ℝ), (∀ (U : ↥(Sobolev.W12 Ω)), (↑↑((↑(E U)).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑((↑U).ofLp 0) x) ∧ ∀ (k : Fin d), ↑↑((↑(E U)).ofLp k.succ) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑((↑U).ofLp k.succ) x) ∧ (∀ (U : ↥(Sobolev.W12 Ω)), ∀ᵐ (y : EuclideanSpace ℝ (Fin d)), y ∉ Ω' → ↑↑((↑(E U)).ofLp 0) y = 0) ∧ ∀ (U : ↥(Sobolev.W12 Ω)), ‖E U‖ ≤ C * ‖U‖

Extension operator between the graph spaces (Guo Theorem III.2.2 at p = 2, Evans §5.4 Theorem 1). On a bounded open domain with C¹ boundary, and for any open set the closure of the domain sits in, there is a bounded linear map from W12 Ω, the H¹(Ω) of this development, to the graph space of the whole space, such that the image of every element agrees with it on the domain, function coordinate and gradient coordinates alike, its function coordinate vanishes almost everywhere outside the given open set, and it is bounded by a constant times the norm of the element.