Extension operator as a linear map

Guo's proof produces an extension of each class. Evans states the same theorem as a bounded linear operator, and this file packages it that way: the partition, the charts, the bounded graphs, the radii and the two cutoffs are all chosen from the domain alone, before any class appears, so the assembled extension is a formula in the class, and every step of that formula is either multiplication by a fixed function, precomposition with a fixed map, or a finite sum.

The domain of the operator is the pair of a class and its gradient, which is what the weak gradient of this development relates; the bound of clause (iii) is stated on that pair, so the operator is bounded in the sense the theorem asserts at every exponent, and not only at 2.

Main declarations

• EllipticPdes.Extension.SobolevPair: a class together with a candidate gradient.
• EllipticPdes.Extension.extLinear: the extension operator, as an ℝ-linear map.
• EllipticPdes.Extension.extLinear_spec: the three clauses of the theorem, stated for that map with a constant quantified before the class.
• EllipticPdes.Extension.exists_extLinear: the theorem as Evans states it, with the operator and the constant produced together.

References

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

@[reducible, inline]

abbrev EllipticPdes.Extension.SobolevPair (d : ℕ) : Type

A class together with a candidate for its gradient. This is the module the extension operator acts on.

Equations

• EllipticPdes.Extension.SobolevPair d = ((EuclideanSpace ℝ (Fin d) → ℝ) × (Fin d → EuclideanSpace ℝ (Fin d) → ℝ))

Linearity of the pieces

theorem EllipticPdes.Extension.indicator_add_apply {α : Type u_1} (s : Set α) (f g : α → ℝ) (y : α) : s.indicator (f + g) y = s.indicator f y + s.indicator g y

The indicator of a set is additive in the function.

theorem EllipticPdes.Extension.indicator_smul_apply {α : Type u_1} (s : Set α) (a : ℝ) (f : α → ℝ) (y : α) : s.indicator (a • f) y = a * s.indicator f y

The indicator of a set commutes with a scalar.

theorem EllipticPdes.Extension.extPiece_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (i : Option ↥P.centres) (u v : EuclideanSpace ℝ (Fin d) → ℝ) : extPiece P i (u + v) = extPiece P i u + extPiece P i v

A piece of the glued extension is additive in the class.

theorem EllipticPdes.Extension.extPiece_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (i : Option ↥P.centres) (a : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : extPiece P i (a • u) = a • extPiece P i u

A piece of the glued extension commutes with a scalar.

theorem EllipticPdes.Extension.extPieceGrad_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (i : Option ↥P.centres) (u v : EuclideanSpace ℝ (Fin d) → ℝ) (g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : extPieceGrad P i (u + v) (g + h) k = extPieceGrad P i u g k + extPieceGrad P i v h k

The gradient of a piece is additive in the class and its gradient together.

theorem EllipticPdes.Extension.extPieceGrad_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (i : Option ↥P.centres) (a : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : extPieceGrad P i (a • u) (a • g) k = a • extPieceGrad P i u g k

The gradient of a piece commutes with a scalar.

Linearity of the glued extension

theorem EllipticPdes.Extension.extFun_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (u v : EuclideanSpace ℝ (Fin d) → ℝ) : extFun P (u + v) = extFun P u + extFun P v

The glued extension is additive in the class.

theorem EllipticPdes.Extension.extFun_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (a : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : extFun P (a • u) = a • extFun P u

The glued extension commutes with a scalar.

theorem EllipticPdes.Extension.extFunGrad_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (u v : EuclideanSpace ℝ (Fin d) → ℝ) (g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : extFunGrad P (u + v) (g + h) k = extFunGrad P u g k + extFunGrad P v h k

The gradient of the glued extension is additive.

theorem EllipticPdes.Extension.extFunGrad_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (a : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : extFunGrad P (a • u) (a • g) k = a • extFunGrad P u g k

The gradient of the glued extension commutes with a scalar.

Linearity of the extension with its support cut down

theorem EllipticPdes.Extension.extSubsetFun_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (χ u v : EuclideanSpace ℝ (Fin d) → ℝ) : extSubsetFun P χ (u + v) = extSubsetFun P χ u + extSubsetFun P χ v

The cut-down extension is additive in the class.

theorem EllipticPdes.Extension.extSubsetFun_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (a : ℝ) (χ u : EuclideanSpace ℝ (Fin d) → ℝ) : extSubsetFun P χ (a • u) = a • extSubsetFun P χ u

The cut-down extension commutes with a scalar.

theorem EllipticPdes.Extension.extSubsetGrad_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (χ u v : EuclideanSpace ℝ (Fin d) → ℝ) (g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : extSubsetGrad P χ (u + v) (g + h) k = extSubsetGrad P χ u g k + extSubsetGrad P χ v h k

The gradient of the cut-down extension is additive.

theorem EllipticPdes.Extension.extSubsetGrad_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (a : ℝ) (χ u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : extSubsetGrad P χ (a • u) (a • g) k = a • extSubsetGrad P χ u g k

The gradient of the cut-down extension commutes with a scalar.

The operator

noncomputable def EllipticPdes.Extension.extLinear {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (χ : EuclideanSpace ℝ (Fin d) → ℝ) : SobolevPair d →ₗ[ℝ] SobolevPair d

Extension operator. A class and its gradient go to the extension and its gradient. The partition, the charts, the graphs, the radii and the cutoff are fixed before the class, so the map is linear.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EllipticPdes.Extension.extLinear_fst {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (χ : EuclideanSpace ℝ (Fin d) → ℝ) (w : SobolevPair d) : ((extLinear P χ) w).1 = extSubsetFun P χ w.1

@[simp]

theorem EllipticPdes.Extension.extLinear_snd {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (P : BoundaryPartition d Ω) (χ : EuclideanSpace ℝ (Fin d) → ℝ) (w : SobolevPair d) (k : Fin d) : ((extLinear P χ) w).2 k = extSubsetGrad P χ w.1 w.2 k

theorem EllipticPdes.Extension.extLinear_spec {d : ℕ} {Ω Ω' : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (P : BoundaryPartition d Ω) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχc : ContDiff ℝ (↑⊤) χ) (hχcs : HasCompactSupport χ) (hχs : tsupport χ ⊆ Ω') (hχ1 : ∀ y ∈ closure Ω, χ y = 1) {p : ENNReal} (hp : 1 ≤ p) : ∃ (K : NNReal), ∀ (w : SobolevPair d), MeasureTheory.IntegrableOn w.1 Ω MeasureTheory.volume → (∀ (k : Fin d), MeasureTheory.IntegrableOn (w.2 k) Ω MeasureTheory.volume) → Embedding.HasWeakGradOn Ω w.1 w.2 → Embedding.HasWeakGradOn Set.univ ((extLinear P χ) w).1 ((extLinear P χ) w).2 ∧ HasCompactSupport ((extLinear P χ) w).1 ∧ tsupport ((extLinear P χ) w).1 ⊆ Ω' ∧ MeasureTheory.Integrable ((extLinear P χ) w).1 MeasureTheory.volume ∧ (∀ (k : Fin d), MeasureTheory.Integrable (((extLinear P χ) w).2 k) MeasureTheory.volume) ∧ (∀ y ∈ Ω, ((extLinear P χ) w).1 y = w.1 y) ∧ MeasureTheory.eLpNorm ((extLinear P χ) w).1 p MeasureTheory.volume ≤ ↑K * (MeasureTheory.eLpNorm w.1 p (MeasureTheory.volume.restrict Ω) + ∑ i : Fin d, MeasureTheory.eLpNorm (w.2 i) p (MeasureTheory.volume.restrict Ω)) ∧ ∀ (k : Fin d), MeasureTheory.eLpNorm (((extLinear P χ) w).2 k) p MeasureTheory.volume ≤ ↑K * (MeasureTheory.eLpNorm w.1 p (MeasureTheory.volume.restrict Ω) + ∑ i : Fin d, MeasureTheory.eLpNorm (w.2 i) p (MeasureTheory.volume.restrict Ω))

Three clauses of the theorem for the operator. The constant is quantified before the class, so the map is bounded in the sense clause (iii) asserts.

theorem EllipticPdes.Extension.exists_extLinear {d : ℕ} {Ω Ω' : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : HasC1Boundary Ω) (hΩ'open : IsOpen Ω') (hsub : closure Ω ⊆ Ω') {p : ENNReal} (hp : 1 ≤ p) : ∃ (T : SobolevPair d →ₗ[ℝ] SobolevPair d) (K : NNReal), ∀ (w : SobolevPair d), MeasureTheory.IntegrableOn w.1 Ω MeasureTheory.volume → (∀ (k : Fin d), MeasureTheory.IntegrableOn (w.2 k) Ω MeasureTheory.volume) → Embedding.HasWeakGradOn Ω w.1 w.2 → Embedding.HasWeakGradOn Set.univ (T w).1 (T w).2 ∧ HasCompactSupport (T w).1 ∧ tsupport (T w).1 ⊆ Ω' ∧ MeasureTheory.Integrable (T w).1 MeasureTheory.volume ∧ (∀ (k : Fin d), MeasureTheory.Integrable ((T w).2 k) MeasureTheory.volume) ∧ (∀ y ∈ Ω, (T w).1 y = w.1 y) ∧ MeasureTheory.eLpNorm (T w).1 p MeasureTheory.volume ≤ ↑K * (MeasureTheory.eLpNorm w.1 p (MeasureTheory.volume.restrict Ω) + ∑ i : Fin d, MeasureTheory.eLpNorm (w.2 i) p (MeasureTheory.volume.restrict Ω)) ∧ ∀ (k : Fin d), MeasureTheory.eLpNorm ((T w).2 k) p MeasureTheory.volume ≤ ↑K * (MeasureTheory.eLpNorm w.1 p (MeasureTheory.volume.restrict Ω) + ∑ i : Fin d, MeasureTheory.eLpNorm (w.2 i) p (MeasureTheory.volume.restrict Ω))

Evans's extension operator (§5.4 Theorem 1, p. 253). On a bounded domain with C¹ boundary, and for any open set the closure of the domain sits in, there is one ℝ-linear map and one constant such that every class with a weak gradient on the domain goes to a class with a weak gradient on the whole space, agreeing with it on the domain, supported inside that open set, and bounded together with its gradient in every Lᵖ seminorm.