Extending a compactly supported weak derivative across the boundary

Extending a weakly differentiable function by zero across ∂Ω destroys weak differentiability in general: the jump along the boundary contributes a singular term that no locally integrable function represents. This file proves that the obstruction is entirely a boundary phenomenon. If u and its weak derivative vanish almost everywhere outside a compact K ⊆ Ω, then the extension of u by zero is weakly differentiable on the whole space, with the zero-extension of the weak derivative as its derivative.

The argument

Test the extension against a test function φ on the whole space. A smooth cutoff χ equal to 1 on a neighbourhood of K and compactly supported inside Ω (IsCompact.exists_contDiff_cutoff) turns χ φ into a test function on Ω, to which the hypothesis applies. The product rule replaces ∂_v (χ φ) by χ ∂_v φ + (∂_v χ) φ, and both correction terms vanish where they are paired with u: off K because u does, and on K because χ is constant there. What is left is the defining identity for the extension.

Nothing is assumed about ∂Ω; the compact support is what replaces boundary regularity. The same statement for a general u ∈ W^{1,p}(Ω) is false, and the extension theorem that repairs it needs a Lipschitz boundary.

Main declarations

• TauCeti.HasWeakLineDerivOn.indicator_of_isCompact: the directional statement.
• TauCeti.HasWeakFDerivOn.indicator_of_isCompact: its Fréchet form.

References

L. C. Evans, Partial Differential Equations, §5.3.3, and H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 9.5.

theorem TauCeti.HasWeakLineDerivOn.indicator_of_isCompact {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} {Omega : TopologicalSpace.Opens E} {u u' : E → F} {v : E} {K : Set E} (h : HasWeakLineDerivOn mu Omega u u' v) (hK : IsCompact K) (hKO : K ⊆ ↑Omega) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, x ∉ K → u x = 0) (hu' : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, x ∉ K → u' x = 0) : HasWeakLineDerivOn mu ⊤ ((↑Omega).indicator u) ((↑Omega).indicator u') v

Extension by zero of a compactly supported weak directional derivative. If u' is a weak derivative of u in the direction v on Ω, and both vanish almost everywhere on Ω outside a compact K ⊆ Ω, then the zero-extension of u' is a weak derivative of the zero-extension of u on the whole space.

No regularity of ∂Ω is used: the cutoff isolating K from ∂Ω is what makes the extension weakly differentiable, and it exists for every open Ω.

theorem TauCeti.HasWeakFDerivOn.indicator_of_isCompact {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} {Omega : TopologicalSpace.Opens E} {u : E → F} {K : Set E} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn mu Omega u U) (hK : IsCompact K) (hKO : K ⊆ ↑Omega) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, x ∉ K → u x = 0) (hU : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, x ∉ K → U x = 0) : HasWeakFDerivOn mu ⊤ ((↑Omega).indicator u) ((↑Omega).indicator U)

Extension by zero of a compactly supported weak Fréchet derivative. The Fréchet form of TauCeti.HasWeakLineDerivOn.indicator_of_isCompact: a weakly differentiable function whose jet vanishes almost everywhere outside a compact subset of Ω extends by zero to a weakly differentiable function on the whole space.