The Sobolev space W^{1,p}_0(Ω) #
This file builds W^{1,p}_0(Ω), the closure of the test functions C_c^∞(Ω) inside the weak
Sobolev space W^{1,p}(Ω) of TauCeti/Analysis/Sobolev/W1p/Basic.lean. This is the
C_c^∞(Ω)-closure half of Lane A.2 of TauCetiRoadmap/PDE/README.md; Meyers--Serrin density is
not proved here.
Test functions as Sobolev functions #
The embedding C_c^∞(Ω) → W^{1,p}(Ω) sends φ to the value-gradient jet (φ, ∇φ), where ∇
is Mathlib's gradient, the Riesz representative of the Fréchet derivative. Two things have to be
checked, and both are easy for a test function: the jet is Lᵖ, because φ and ∇φ are
continuous with compact support; and the weak-derivative identity holds, because ∇φ represents
the classical derivative, which is a weak derivative by
TauCeti.hasWeakFDerivOn_of_differentiableOn. The embedding is linear
(TauCeti.W1p.ofTestFunctionₗ), which is what makes its range a subspace.
Why the closure, and why not all of W^{1,p}(Ω) #
W^{1,p}_0(Ω) is defined as TauCeti.w1p0Submodule, the topological closure of that range. It is
the Sobolev-space stand-in for the homogeneous Dirichlet boundary condition u|_{∂Ω} = 0: no
boundary regularity of Ω is assumed, and no trace operator is needed to state it. The
distinction from W^{1,p}(Ω) is real: for example, the Poincaré inequality holds on this closed
subspace under a suitable geometric hypothesis but not on all of W^{1,p}(Ω).
Main declarations #
TauCeti.W1p.ofTestFunctionₗandTauCeti.W1p.ofTestFunctionₗ_injective: the linear embeddingC_c^∞(Ω) → W^{1,p}(Ω), and its injectivity.TauCeti.w1p0SubmoduleandTauCeti.W1p0: the spaceW^{1,p}_0(Ω), complete for the graph norm.TauCeti.W1p0.valueL: the canonical continuous value map intoLᵖ(Ω).TauCeti.W1p0.denseRange_valueL_two: test functions make the value map fromW^{1,2}_0(Ω)dense inL²(Ω), andTauCeti.W1p0.valueL_ne_zero: on a nonemptyΩthe value map is nonzero for everyp.TauCeti.w1p0Submodule_subset_of_isClosed: a closed set containing every test-function jet containsW^{1,p}_0(Ω), which is how a property is extended from test functions to the whole space.
References #
The C_c^∞(Ω)-closure half of Lane A.2 of TauCetiRoadmap/PDE/README.md; L. C. Evans,
Partial Differential Equations, Section 5.2.
Test functions as Sobolev functions #
The test functions inside W^{1,p}(Ω): the linear embedding sending φ ∈ C_c^∞(Ω) to the
value-gradient jet (φ, ∇φ). Linearity is what makes the range a subspace, hence its closure
TauCeti.w1p0Submodule a subspace too.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The embedding of the test functions is injective: two test functions with the same jet
agree almost everywhere on Ω, hence everywhere, being continuous, supported in Ω, and measured
by a Haar measure, which is positive on nonempty open sets. So W^{1,p}(Ω) really does contain a
copy of C_c^∞(Ω), not just a quotient of it.
The space W^{1,p}_0(Ω) #
The closed subspace W^{1,p}_0(Ω) of W^{1,p}(Ω): the closure of the test functions
C_c^∞(Ω), the Sobolev formulation of the homogeneous Dirichlet boundary condition. No
regularity, and no boundedness, of Ω is assumed.
Equations
- TauCeti.w1p0Submodule mu Omega p = (TauCeti.W1p.ofTestFunctionₗ mu Omega p).range.closure
Instances For
W^{1,p}_0(Ω) is the closure of the set of test-function jets.
A test function, viewed in W^{1,p}(Ω), lies in W^{1,p}_0(Ω).
Minimality of the closure: a closed set containing every test-function jet contains all
of W^{1,p}_0(Ω).
The Sobolev space W^{1,p}_0(Ω), the closure of C_c^∞(Ω) in W^{1,p}(Ω).
Equations
- TauCeti.W1p0 mu Omega p = ↑(TauCeti.w1p0Submodule mu Omega p)
Instances For
Shortcut instance for the norm W^{1,p}_0(Ω) inherits through the two nested Sobolev
subspaces; instance search does not find it on its own.
Shortcut instance for the scalar action W^{1,p}_0(Ω) inherits through the two nested
Sobolev subspaces.
Equations
The canonical value map of W^{1,p}_0(Ω), the value component of the Sobolev jet read
off a zero-boundary function, as a continuous linear map into Lᵖ(Ω).
Equations
- TauCeti.W1p0.valueL = TauCeti.W1p.valueL ∘SL (↑(TauCeti.w1p0Submodule mu Omega p)).subtypeL
Instances For
The value map W^{1,2}_0(Ω) → L²(Ω) has dense range. Indeed, its range contains
all test functions, and an L² function orthogonal to every test function vanishes almost
everywhere by the fundamental lemma of the calculus of variations.
A nonempty open set contains a zero-boundary Sobolev function with nonzero Lᵖ value.
On a nonempty open set the value map W^{1,p}_0(Ω) → Lᵖ(Ω) is nonzero: it does not kill the
test function of TauCeti.W1p0.exists_value_ne_zero.
W^{1,p}_0(Ω) is complete: it is a closed subspace of the complete space W^{1,p}(Ω).