Compactly supported Sobolev functions have zero boundary values #
W^{1,p}_0(Ω) is the closure of the test functions C_c^∞(Ω) in W^{1,p}(Ω), the Sobolev form
of the homogeneous Dirichlet condition. Deciding that a given function lies in it is, in
general, a boundary question. This file settles the case in which there is no boundary to
answer for: if u ∈ W^{1,p}(Ω) vanishes almost everywhere outside a compact K ⊆ Ω, then
u ∈ W^{1,p}_0(Ω).
Only the value component is assumed to vanish; the gradient then vanishes off K by itself,
because a Sobolev function that vanishes on an open set has vanishing weak gradient there
(TauCeti.W1p.gradient_ae_eq_zero_of_value_ae_eq_zero).
The argument #
Extending u by zero gives a genuine element of W^{1,p}(ℝⁿ)
(TauCeti.HasWeakFDerivOn.indicator_of_isCompact), which is where the compact support is used:
for a general u ∈ W^{1,p}(Ω) the zero-extension need not be weakly differentiable at all. On
the whole space every Sobolev function is a limit of test functions
(TauCeti.W1p.mem_w1p0Submodule_top), but those test functions are supported anywhere in ℝⁿ,
so they do not exhibit u as a limit of test functions on Ω. Multiplying by a cutoff χ
which is 1 on K and compactly supported inside Ω repairs that: it leaves the extension of
u unchanged, while carrying every test function on ℝⁿ into the image of C_c^∞(Ω). Since
that image is closed — extension by zero is an isometry of W^{1,p}_0(Ω) onto its image — the
limit stays in it, and restricting the isometry back gives u itself.
Consequences #
TauCeti.W1p.contDiffSMul_mem_w1p0Submodule_of_hasCompactSupport is the form localization
arguments use: multiplying any u ∈ W^{1,p}(Ω) by a smooth cutoff compactly supported in Ω
produces an element of W^{1,p}_0(Ω). The companion
TauCeti.W1p.contDiffSMul_mem_w1p0Submodule needs u to lie in W^{1,p}_0(Ω) already, which is
exactly what the compact support replaces here. This is the localization step of Meyers--Serrin
density and of interior estimates.
Main declarations #
TauCeti.W1p.mem_w1p0Submodule_of_isCompact: a compactly supported Sobolev function has zero boundary values.TauCeti.W1p.contDiffSMul_mem_w1p0Submodule_of_hasCompactSupport: multiplication by a compactly supported cutoff lands inW^{1,p}_0(Ω).TauCeti.W1p.value_extendByZeroL_contDiffSMul_aeandTauCeti.W1p.gradient_extendByZeroL_contDiffSMul_ae: the value and weak gradient of a cutoff product extended by zero to the whole space.TauCeti.W1p.exists_top_value_gradient_ae_eq_on_of_isCompact: near a compact subset ofΩ, a function inW^{1,p}(Ω)agrees in value and gradient with one inW^{1,p}(ℝⁿ).
References #
L. C. Evans, Partial Differential Equations, §5.3.3; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 9.5.
Zero boundary values #
A compactly supported Sobolev function lies in W^{1,p}_0(Ω). If u ∈ W^{1,p}(Ω)
vanishes almost everywhere outside a compact K ⊆ Ω, then u is a W^{1,p}-limit of test
functions on Ω.
No regularity of ∂Ω is assumed, and none is needed: the hypothesis keeps u away from the
boundary, so a cutoff can separate it from ∂Ω.
Multiplication by a compactly supported cutoff #
Multiplying by a cutoff compactly supported in Ω lands in W^{1,p}_0(Ω). Unlike
TauCeti.W1p.contDiffSMul_mem_w1p0Submodule, nothing is assumed about the boundary behaviour of
u: the support of ψ keeps the product away from ∂Ω. This is the localization device that
turns a statement about W^{1,p}(Ω) into one about the test-function closure.
Localisation to the whole space #
The value of an extended cutoff product. For ψ smooth and u ∈ W^{1,p}(Ω) with
ψ u ∈ W^{1,p}_0(Ω), the extension of ψ u by zero to the whole space is ψ u on Ω and
vanishes off Ω.
The Leibniz rule for an extended cutoff product. For ψ smooth and u ∈ W^{1,p}(Ω)
with ψ u ∈ W^{1,p}_0(Ω), the extension of ψ u by zero to the whole space has weak gradient
ψ ∇u + u ∇ψ on Ω and 0 off Ω.
Localisation to the whole space. For 1 ≤ p < ∞, a Sobolev function u ∈ W^{1,p}(Ω)
agrees, in value and in gradient, almost everywhere on any compact S ⊆ Ω with some
w ∈ W^{1,p}(ℝⁿ). One may take for w the product of u with a smooth cutoff equal to one near
S and compactly supported in Ω, extended by zero.