Iterated weak derivatives pass to a smaller region

The induction of Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) runs on a pair V ⋐ W ⋐ Ω: the cutoff lives on W, the conclusion is asked on V, and the datum's regularity is established on whichever of the two is convenient. Moving a family between them is the bookkeeping this file removes.

A weak derivative on W is tested against every test function supported in W, and a test function supported in V ⊆ W is one of them. Both integrals then localise to V, since the integrands vanish off the support. The bound comes along because extension by zero preserves the norm and restriction does not increase it.

Main declarations

• HasWeakDerivOn.restrict: a weak derivative on W restricts to one on V ⊆ W.
• HasIteratedWeakDerivOn.restrict: the family.
• IteratedL2Bound.restrict: the bound, with the same constant.

theorem EllipticPdes.Regularity.HasWeakDerivOn.restrict {d : ℕ} {W V : Set (EuclideanSpace ℝ (Fin d))} {ℓ : Fin d} (hWm : MeasurableSet W) (hVm : MeasurableSet V) (hVW : V ⊆ W) {g g' : Sobolev.L2D W} (h : HasWeakDerivOn W ℓ g g') : HasWeakDerivOn V ℓ (restrictL2 ((extendL2 hWm) g)) (restrictL2 ((extendL2 hWm) g'))

Restriction of a weak derivative to a smaller region. Test functions supported in V are test functions supported in W, and each integral over W collapses to one over V because its integrand vanishes off the support.

noncomputable def EllipticPdes.Regularity.HasIteratedWeakDerivOn.restrict {d : ℕ} {W V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} (hWm : MeasurableSet W) (hVm : MeasurableSet V) (hVW : V ⊆ W) {g : Sobolev.L2D W} (hg : HasIteratedWeakDerivOn W k g) : HasIteratedWeakDerivOn V k (restrictL2 ((extendL2 hWm) g))

The order-k family on a smaller region, entry by entry.

Equations

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

theorem EllipticPdes.Regularity.IteratedL2Bound.restrict {d : ℕ} {W V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {hWm : MeasurableSet W} {hVm : MeasurableSet V} {hVW : V ⊆ W} {g : Sobolev.L2D W} {hg : HasIteratedWeakDerivOn W k g} {C : ℝ} (hC : IteratedL2Bound hg C) : IteratedL2Bound (HasIteratedWeakDerivOn.restrict hWm hVm hVW hg) C

The restricted family has the same bound: extension by zero preserves the norm and restriction does not increase it.