Extending a W^{1,p}_0 function by zero #
A function in W^{1,p}(Ω) has no reason to stay Sobolev when it is extended by zero across ∂Ω:
without some condition forcing it to vanish towards the boundary, the extension can fail to be
weakly differentiable on the larger set at all. For W^{1,p}_0(Ω), the closure of C_c^∞(Ω),
that obstruction disappears, and this file proves it: the zero-extension of a W^{1,p}_0(Ω)
function to any larger open set Ω' lies in W^{1,p}_0(Ω'), and its weak gradient is the
zero-extension of the original weak gradient.
This is the boundary-regularity-free half of Lane A.6 of TauCetiRoadmap/PDE/README.md. Taking
Ω' = ⊤ gives the extension operator W^{1,p}_0(Ω) → W^{1,p}(ℝⁿ) that lane asks for, which is
what lets whole-space statements (Gagliardo--Nirenberg--Sobolev, translation estimates, and
through them Rellich--Kondrachov) be applied to functions given on a domain. The extension
operator for W^{1,p}(Ω) itself is a genuinely harder theorem needing Lipschitz ∂Ω, and is not
proved here.
The argument #
Everything rests on TauCeti.w1p0Submodule_subset_of_isClosed: the zero-extension map is
continuous, and the property "the extension is a test-function limit on Ω'" is closed, so it is
enough to check it on test functions. For a test function it is immediate, because a test
function on Ω is a test function on Ω' — TestFunction.monoCLM — and extending it by zero
does not change it at all: it already vanished off Ω, as did its gradient.
The zero-extension itself is TauCeti.extendByZeroLpₗᵢ, applied once to the value component,
once to the gradient component, and once to the value-gradient jet that carries both. It is an
isometry of Lᵖ spaces, so the extension operator is an isometry of Sobolev spaces:
TauCeti.W1p0.norm_extendByZeroL.
Main declarations #
TauCeti.Sobolev1JetLp.extendByZeroₗᵢ: extension by zero of anLᵖvalue-gradient jet.TauCeti.Sobolev1JetLp.extendByZeroₗᵢ_mem_w1pSubmodule: the zero-extension of aW^{1,p}_0(Ω)function is a Sobolev function onΩ'.TauCeti.W1p0.extendByZeroL: the extension operatorW^{1,p}_0(Ω) →L[ℝ] W^{1,p}_0(Ω'), withTauCeti.W1p0.norm_extendByZeroLand its value and gradient components; it is functorial inΩbyTauCeti.W1p0.extendByZeroL_selfandTauCeti.W1p0.extendByZeroL_extendByZeroL.TauCeti.W1p0.value_extendByZeroL_ae_eq_zero_compl: the whole-space extension vanishes almost everywhere offΩ.TauCeti.W1p0.hasWeakFDerivOn_indicator: the analytic content, that the zero-extension ofuis weakly differentiable onΩ'with the zero-extension of∇uas its weak gradient.
References #
Lane A.6 of TauCetiRoadmap/PDE/README.md; L. C. Evans, Partial Differential Equations,
Section 5.5, and H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential
Equations, Lemma 9.5.
Extension by zero of Lᵖ jets #
Extension by zero of an Lᵖ value-gradient jet from Ω to a larger open set Ω': both
components are declared zero on Ω' \ Ω. It is an isometry, since the added region contributes
nothing to the Lᵖ norm of the jet: both of its components vanish there.
Equations
Instances For
The extension of a jet is the indicator of the original jet.
The value component of an extended jet is the extension of the value component: taking a
component is a pointwise postcomposition, and TauCeti.coeFn_extendByZeroLpₗᵢ_comp says that
those commute with extension by zero.
The gradient component of an extended jet is the extension of the gradient component; as for
TauCeti.Sobolev1JetLp.value_extendByZeroₗᵢ, this is postcomposition commuting with extension.
Test functions extend to test functions #
The zero-extension of a test-function jet is the jet of the same test function on the larger open set.
The extension theorem #
The zero-extension of a W^{1,p}_0(Ω) function is a Sobolev function on Ω'. No
regularity of ∂Ω is needed, and no boundedness of either open set; the boundary condition
carried by membership in W^{1,p}_0(Ω) is what makes the extension weakly differentiable.
Extension by zero as an operator W^{1,p}_0(Ω) →L[ℝ] W^{1,p}_0(Ω'). The extension of a
limit of test functions on Ω is again a limit of test functions, on Ω', so the operator lands
in W^{1,p}_0(Ω') and not merely in W^{1,p}(Ω'); compose with
(TauCeti.w1p0Submodule mu Omega' p).toSubmodule.subtypeL for the W^{1,p}(Ω')-valued map.
Taking Ω' = ⊤, that is hsub = le_top, gives the extension operator to the whole space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ambient jet of the extension is the extension of the ambient jet.
Extending by zero from Ω to Ω does nothing.
Extending by zero twice is extending by zero once.
Extension by zero is an isometry of Sobolev spaces. The W^{1,p} norm — the Lᵖ norm
of the value-gradient jet — is unchanged; the extension adds a region on which both components
vanish.
The value component of the extension is the zero-extension of the value component.
The value component of the whole-space zero extension of u ∈ W^{1,p}_0(Ω) vanishes almost
everywhere off Ω. Thus its support is contained in Ω up to a null set; when Ω is bounded,
this is the fixed-bounded-support input for Fréchet--Kolmogorov.
The gradient component of the extension is the zero-extension of the gradient component.
The analytic content of the extension theorem. The zero-extension of u ∈ W^{1,p}_0(Ω)
is weakly differentiable on the larger open set Ω', with weak gradient the zero-extension of the
weak gradient of u. This is the statement that can fail for a general u ∈ W^{1,p}(Ω): with
no condition forcing u to vanish towards ∂Ω, its zero-extension need not be weakly
differentiable on Ω' at all.