Identifications on the collar

The inductive hypothesis of Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) hands over a family of iterated weak derivatives on a compact set, and says of its first entries only that they are weak derivatives of the solution. The ambient element has its own first derivatives, in its gradient coordinates. The two agree, but only almost everywhere, and only where a cutoff is invisible.

EllipticPdes.Regularity.mulTest_weakDerivOn_unique gives the agreement after a cutoff. On an open collar where the outer cutoff of the tower is identically 1, the cutoff drops out and the two families become equal as L² classes on the collar. Running the induction step there rather than on the compact set is what lets a single family supply every derivative the datum needs.

Main declarations

• restrictL2_extendL2_trans: restricting twice is restricting once.
• restrictL2_extendL2_eq_of_mulTest_eq: an identification after a cutoff becomes an equality on the collar.
• restrictL2_extendL2_congr_of_weakDerivOn: two weak derivatives of one class are equal on the collar.
• exists_restrictFamily, exists_collarFamily: a family and its bound, moved in one step.

theorem EllipticPdes.Regularity.restrictL2_extendL2_trans {d : ℕ} {Ω W N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hNm : MeasurableSet N) (hNW : N ⊆ W) (g : Sobolev.L2D Ω) : restrictL2 ((extendL2 hWm) (restrictL2 ((extendL2 hΩm) g))) = restrictL2 ((extendL2 hΩm) g)

Restricting twice is restricting once. For N ⊆ W, cutting an L²(Ω) class down to W and then to N is cutting it down to N. The two sets need no relation to Ω, since the whole-space extension is what both restrictions read.

theorem EllipticPdes.Regularity.restrictL2_extendL2_eq_of_mulTest_eq {d : ℕ} {W N : Set (EuclideanSpace ℝ (Fin d))} (hWm : MeasurableSet W) (hNm : MeasurableSet N) (hNW : N ⊆ W) {θ : EuclideanSpace ℝ (Fin d) → ℝ} (hθW : Sobolev.IsTestFn W θ) (hθN : Set.EqOn θ 1 N) {X Y : Sobolev.L2D W} (h : (mulTest hθW) X = (mulTest hθW) Y) : restrictL2 ((extendL2 hWm) X) = restrictL2 ((extendL2 hWm) Y)

Identification after a cutoff as an equality on the collar. Where θ is identically 1 on N ⊆ W, two classes with θ·X = θ·Y restrict to the same class on N.

theorem EllipticPdes.Regularity.restrictL2_extendL2_congr_of_weakDerivOn {d : ℕ} {W N : Set (EuclideanSpace ℝ (Fin d))} (hWm : MeasurableSet W) (hNm : MeasurableSet N) (hNW : N ⊆ W) {θ : EuclideanSpace ℝ (Fin d) → ℝ} (hθW : Sobolev.IsTestFn W θ) (hθN : Set.EqOn θ 1 N) {i : Fin d} {g X Y : Sobolev.L2D W} (hX : HasWeakDerivOn W i g X) (hY : HasWeakDerivOn W i g Y) : restrictL2 ((extendL2 hWm) X) = restrictL2 ((extendL2 hWm) Y)

Two weak derivatives of one class are equal on the collar. The inductive family's first entries and the ambient element's gradient coordinates are both weak derivatives of the solution, so they agree there.

theorem EllipticPdes.Regularity.exists_restrictFamily {d : ℕ} {Ω N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hNm : MeasurableSet N) (hNΩ : N ⊆ Ω) {g : Sobolev.L2D Ω} {k : ℕ} {C : ℝ} (H : HasIteratedWeakDerivOn Ω k g) (hC : IteratedL2Bound H C) : ∃ (HN : HasIteratedWeakDerivOn N k (restrictL2 ((extendL2 hΩm) g))), IteratedL2Bound HN C

Family and its bound moved to a subregion. Both halves of the restriction, packaged so the elaborator does the unification once. Applied inline in the induction step, where the context has the tower and the datum, the same two lines take minutes.

theorem EllipticPdes.Regularity.exists_collarFamily {d : ℕ} {Ω W N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hNm : MeasurableSet N) (hNW : N ⊆ W) {θ : EuclideanSpace ℝ (Fin d) → ℝ} (hθW : Sobolev.IsTestFn W θ) (hθN : Set.EqOn θ 1 N) {g : Sobolev.L2D Ω} {Dg : Fin d → Sobolev.L2D Ω} (hDgw : ∀ (i : Fin d), HasWeakDeriv i ((extendL2 hΩm) g) ((extendL2 hΩm) (Dg i))) {m : ℕ} {C : ℝ} (HuW : HasIteratedWeakDerivOn W (m + 1) (restrictL2 ((extendL2 hΩm) g))) (hHuW : IteratedL2Bound HuW C) : ∃ (HuN : HasIteratedWeakDerivOn N (m + 1) (restrictL2 ((extendL2 hΩm) g))), IteratedL2Bound HuN C ∧ ∀ (i : Fin d), HuN.D [i] = restrictL2 ((extendL2 hΩm) (Dg i))

Inductive family moved to the collar. A family on W for the whole-space extension of g, restricted to N, is a family there for the same class, with the same bound, and its first entries are the given weak derivatives of g.

The three conclusions travel together because the induction step needs all three and each is a unification the elaborator should do once. Doing them inline takes minutes, since the step's context has the tower, its collar, four cutoffs and the datum by the time it needs them.