Cutoff transport of weak derivatives to the ambient domain

The induction of Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) runs on a pair V ⋐ W ⋐ Ω. The order-k conclusion is available on the compact W, and the datum the induction hypothesis consumes needs its weak derivatives on all of Ω. EllipticPdes.Regularity.HasIteratedWeakDerivOn.restrict moves a family the other way, from W down to a smaller set, and is no help here.

Extension by zero is what closes the gap, and it needs the function to vanish near the boundary of W. A cutoff supplies that: for a test function χ supported in W, the product χ · p extended by zero to Ω has as many weak derivatives on Ω as p has on W.

Keystone identity

Against a test function φ supported in Ω, the product χ · φ is a test function supported in tsupport χ ⊆ W, so the weak derivative of p on W may be tested against it:

∫_W p ∂_ℓ(χφ) = - ∫_W p' χφ.

Expanding ∂_ℓ(χφ) = (∂_ℓχ)φ + χ(∂_ℓφ) and moving the first summand across gives

∫_W (χp) ∂_ℓφ = - ∫_W ((∂_ℓχ)p + χp') φ,

and both sides may be read over Ω instead of W, since χ kills the integrand off W. That is the statement that (∂_ℓχ)p + χp' is the weak ℓ-derivative of χp on Ω. Nothing about ∂W is needed, and no extension operator on Sobolev spaces appears: the cutoff does all the work.

Order-k family

The recursion is the one EllipticPdes.Regularity.exists_iteratedWeakDeriv_mul uses. The ℓ-derivative of χ·p is (∂_ℓχ)·p + χ·(∂_ℓp), and each summand is again a test function supported in W against a function with k weak derivatives on W, so the statement recurses on its own conclusion. Test functions are closed under partialD, which is what lets the weight change at each step without leaving the hypothesis.

Main declarations

• isTestFn_partialD: test functions are closed under a classical partial derivative.
• setIntegral_mul_mulTest_partialD: the integration by parts the cutoff makes admissible.
• HasWeakDerivOn.extend_mulTest: one weak derivative, from W to Ω, across a cutoff.
• hasWeakDeriv_extend_mulTest: the same, on the whole space.
• exists_iteratedWeakDeriv_extend_mulTest: the order-k family and its bound.

Test functions are closed under a partial derivative

theorem EllipticPdes.Regularity.isTestFn_partialD {d : ℕ} {W : Set (EuclideanSpace ℝ (Fin d))} {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn W χ) (ℓ : Fin d) : Sobolev.IsTestFn W (Sobolev.partialD ℓ χ)

A classical partial derivative of a test function is a test function on the same set.

Integration by parts the cutoff makes admissible

theorem EllipticPdes.Regularity.setIntegral_mul_mulTest_partialD {d : ℕ} {W : Set (EuclideanSpace ℝ (Fin d))} {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn W χ) {ℓ : Fin d} {p p' : Sobolev.L2D W} (h : HasWeakDerivOn W ℓ p p') {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in W, ↑↑p x * (χ x * Sobolev.partialD ℓ φ x) = -∫ (x : EuclideanSpace ℝ (Fin d)) in W, (Sobolev.partialD ℓ χ x * ↑↑p x + χ x * ↑↑p' x) * φ x

Integration by parts against a cut-off test function. For χ supported in W and a weak ℓ-derivative p' of p on W,

∫_W p · (χ ∂_ℓφ) = - ∫_W ((∂_ℓχ)p + χp') · φ

for every smooth φ, asking neither compact support nor a support condition of it. The product χφ is compactly supported in tsupport χ ⊆ W whatever φ does, so it is admissible for the weak derivative, and expanding ∂_ℓ(χφ) moves the term where the derivative lands on the cutoff across.

This is the one identity the cutoff gives, and everything else in this file and in Evans's step 3 is bookkeeping around it.

One derivative across the cutoff

theorem EllipticPdes.Regularity.HasWeakDerivOn.extend_mulTest {d : ℕ} {W Ω : Set (EuclideanSpace ℝ (Fin d))} (hWm : MeasurableSet W) (hWΩ : W ⊆ Ω) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn W χ) {ℓ : Fin d} {p p' : Sobolev.L2D W} (h : HasWeakDerivOn W ℓ p p') {q q' : Sobolev.L2D Ω} (hq : ↑↑q =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => χ x * ↑↑((extendL2 hWm) p) x) (hq' : ↑↑q' =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => Sobolev.partialD ℓ χ x * ↑↑((extendL2 hWm) p) x + χ x * ↑↑((extendL2 hWm) p') x) : HasWeakDerivOn Ω ℓ q q'

Transport of one weak derivative from W up to Ω by a cutoff. For a test function χ supported in W ⊆ Ω and a weak ℓ-derivative p' of p on W, any L²(Ω) class representing χ·p has (∂_ℓχ)·p + χ·p' as its weak ℓ-derivative on Ω.

The classes are given through a.e. representations rather than as named products, matching EllipticPdes.Regularity.norm_le_of_ae_mul, because the consumers assemble their own.

The proof tests the W-derivative against χφ, which is admissible because χ is supported in W, and reads the Leibniz expansion of ∂_ℓ(χφ) backwards. Each integral over Ω becomes one over W because χ vanishes off its support.

theorem EllipticPdes.Regularity.hasWeakDeriv_extend_mulTest {d : ℕ} {W : Set (EuclideanSpace ℝ (Fin d))} (hWm : MeasurableSet W) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn W χ) {ℓ : Fin d} {p p' : Sobolev.L2D W} (h : HasWeakDerivOn W ℓ p p') {q q' : ↥(MeasureTheory.EucL2 d)} (hq : ↑↑q =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => χ x * ↑↑((extendL2 hWm) p) x) (hq' : ↑↑q' =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => Sobolev.partialD ℓ χ x * ↑↑((extendL2 hWm) p) x + χ x * ↑↑((extendL2 hWm) p') x) : HasWeakDeriv ℓ q q'

Transport of one weak derivative from W up to the whole space by a cutoff. The same identity as HasWeakDerivOn.extend_mulTest with the ambient set taken to be everything, which is the form EllipticPdes.Regularity.HasWeakDeriv.unique consumes.

Stated separately rather than instantiated, because L²(univ) and L²(ℝᵈ) are different types and the conversion is longer than the proof.

Order-k family across the cutoff

theorem EllipticPdes.Regularity.exists_iteratedWeakDeriv_extend_mulTest {d : ℕ} {W Ω : Set (EuclideanSpace ℝ (Fin d))} (hWm : MeasurableSet W) (hWΩ : W ⊆ Ω) (k : ℕ) {χ : EuclideanSpace ℝ (Fin d) → ℝ} : Sobolev.IsTestFn W χ → ∃ (K : ℝ), 0 ≤ K ∧ ∀ {p : Sobolev.L2D W} (hp : HasIteratedWeakDerivOn W k p) {q : Sobolev.L2D Ω}, (↑↑q =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => χ x * ↑↑((extendL2 hWm) p) x) → ∀ {M : ℝ}, IteratedL2Bound hp M → ∃ (H : HasIteratedWeakDerivOn Ω k q), IteratedL2Bound H (K * M)

Transport of k weak derivatives from W up to Ω by a cutoff. For a test function χ supported in W ⊆ Ω there is a constant K, depending on χ and k alone, such that whenever p has weak derivatives to order k on W bounded by M, every L²(Ω) class representing χ·p has weak derivatives to order k on Ω bounded by K·M.

The induction is on k, with the weight quantified inside so that it may change at each step. HasWeakDerivOn.extend_mulTest supplies the single derivative ∂_ℓ(χ·p) = (∂_ℓχ)·p + χ·(∂_ℓp), and the induction hypothesis covers each summand: the first with the weight ∂_ℓχ, again a test function supported in W, and the second with the function ∂_ℓp, whose order-k family is HasIteratedWeakDerivOn.deriv.