Gradient of a cut-off function in closed form

EllipticPdes.Regularity.interior_cutoffGrad_mem_H01 puts ξ·∂_ℓu in H₀¹(Ω) and says that the gradient coordinates of the resulting element are its weak derivatives. It says nothing about what they are, because the element is produced as a weak limit of difference quotients and the limit has no formula.

Evans's step 3 needs the formula. Expanding B[ξ·∂_ℓu, w] asks for ∂ᵢ(ξ·∂_ℓu) as a sum of a term where the derivative lands on the cutoff and a term where it lands on the solution, and only the second meets the differentiated equation.

The Leibniz rule across the cutoff supplies the candidate, and uniqueness of the whole-space weak derivative identifies it with the coordinate. HasWeakDeriv.unique is the whole-space statement, which is why hasWeakDeriv_extend_mulTest is stated on the whole space rather than on Ω.

Main declarations

• extendL2_restrictL2_extendL2_ae: cutting an L²(Ω) class down to W ⊆ Ω and extending again is the indicator of W.
• extendL2_mulTest_eq: a cut-off class is the cut-off restriction.
• extendL2_cutoffGrad_eq: the gradient coordinates of the cut-off element, in closed form.

theorem EllipticPdes.Regularity.extendL2_restrictL2_extendL2_ae {d : ℕ} {Ω W : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hWΩ : W ⊆ Ω) (g : Sobolev.L2D Ω) : ↑↑((extendL2 hWm) (restrictL2 ((extendL2 hΩm) g))) =ᵐ[MeasureTheory.volume] W.indicator fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑g x

Cutting down and extending again is the indicator. For W ⊆ Ω, restricting an L²(Ω) class to W and extending by zero gives the indicator of W applied to the class.

theorem EllipticPdes.Regularity.extendL2_mulTest_eq {d : ℕ} {Ω W : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hWΩ : W ⊆ Ω) {ξ : EuclideanSpace ℝ (Fin d) → ℝ} (hξΩ : Sobolev.IsTestFn Ω ξ) (hξW : Sobolev.IsTestFn W ξ) (g : Sobolev.L2D Ω) : (extendL2 hΩm) ((mulTest hξΩ) g) = (extendL2 hWm) ((mulTest hξW) (restrictL2 ((extendL2 hΩm) g)))

Cut-off class as the cut-off restriction. For a cutoff supported in W ⊆ Ω, the whole-space extension of ξ·g is the whole-space extension of ξ against the restriction of g to W. The cutoff kills everything outside W, so nothing is lost.

This is the function coordinate of extendL2_cutoffGrad_eq, stated on its own because the zeroth-order block of the induction step needs exactly it.

theorem EllipticPdes.Regularity.extendL2_cutoffGrad_eq {d : ℕ} {Ω W : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hWΩ : W ⊆ Ω) {ξ : EuclideanSpace ℝ (Fin d) → ℝ} (hξΩ : Sobolev.IsTestFn Ω ξ) (hξW : Sobolev.IsTestFn W ξ) (g : Sobolev.L2D Ω) {Uamb : Sobolev.H1amb Ω} (hUgrad : ∀ (i : Fin d), HasWeakDeriv i ((extendL2 hΩm) ((mulTest hξΩ) g)) ((extendL2 hΩm) (Uamb.ofLp i.succ))) {Dg : Fin d → Sobolev.L2D W} (hDg : ∀ (i : Fin d), HasWeakDerivOn W i (restrictL2 ((extendL2 hΩm) g)) (Dg i)) (i : Fin d) : (extendL2 hΩm) (Uamb.ofLp i.succ) = (extendL2 hWm) ((mulTest ⋯) (restrictL2 ((extendL2 hΩm) g)) + (mulTest hξW) (Dg i))

Gradient of a cut-off class in closed form. Let ξ be a cutoff supported in W ⊆ Ω, let g ∈ L²(Ω) have weak derivatives Dg i on W, and let Uamb be an ambient element whose function coordinate is ξ·g and whose gradient coordinates are the weak derivatives of that product. Then each gradient coordinate is (∂ᵢξ)·g + ξ·(∂ᵢg).

The Leibniz rule across the cutoff (hasWeakDeriv_extend_mulTest) shows the right-hand side to be a weak i-derivative of ξ·g, and the coordinate is one by hypothesis, so HasWeakDeriv.unique identifies them. Both sides are extensions by zero from W, which is where the derivative of g is known and where the cutoff lives.