The Sobolev spaces W^{k,p}_0(Ω) #
This file constructs TauCeti.Wkp0 μ Ω p k, the closure of the smooth compactly supported
functions in the arbitrary-order weak Sobolev space TauCeti.Wkp μ Ω p k. It extends the
first-order construction TauCeti.W1p0; the equality
TauCeti.wkp0Submodule_one verifies that the two closed subspaces agree at order one.
A test function enters W^{k,p} together with all of its classical derivatives through order
k. The derivative field of index j is the (j+1)-st classical derivative, valued in
TauCeti.IteratedGradient E j; index zero is Mathlib's gradient, identified with the derivative
by the real inner product, and every successor is a Fréchet derivative. Each field is smooth and
compactly supported, hence belongs to every Lᵖ space, and a classical derivative is a weak
derivative by TauCeti.hasWeakFDerivOn_of_differentiableOn. This produces the injective linear
map TauCeti.Wkp.ofTestFunctionₗ, whose range is then closed to define TauCeti.wkp0Submodule.
No boundedness or boundary regularity of Ω is required. Meyers--Serrin density of smooth
Sobolev functions and density results comparing different domains are not proved here.
Main declarations #
TauCeti.iteratedGradientTestFunction: the recursively bundled classical derivatives of a test function.TauCeti.Wkp.ofTestFunctionₗ: the injective linear embeddingC_c^∞(Ω) → W^{k,p}(Ω).TauCeti.wkp0SubmoduleandTauCeti.Wkp0: the closure of the test functions inW^{k,p}(Ω)and its complete normed-space type.TauCeti.Wkp0.ofTestFunctionₗandTauCeti.Wkp0.lowerOrderL: the dense test-function inclusion and the lower-order projection with zero-boundary codomains.TauCeti.wkp0Submodule_subset_of_isClosed: the closure induction principle used to extend a closed property from test functions toW^{k,p}_0(Ω).
References #
This is the arbitrary-order C_c^∞(Ω)-closure part of Lane A.2 in
TauCetiRoadmap/PDE/README.md. The construction follows L. C. Evans, Partial Differential
Equations, Section 5.2.
Test functions and their iterated gradients #
The classical derivative fields of a test function, indexed so that index zero is its gradient and each successor is the Fréchet derivative of the preceding field.
Equations
- TauCeti.iteratedGradientTestFunction phi k = TauCeti.iteratedGradientChain (⇑phi) k
Instances For
The derivative fields of a test function are its classical iterated-gradient chain.
This bridge is intentionally not a simp lemma: test-function fields are the normal form used
by the zero, successor, and Lᵖ representative simp lemmas below.
Every iterated gradient of a test function is smooth.
Every iterated gradient of a test function has compact support.
Every iterated gradient of a test function belongs to Lᵖ(Ω) for every exponent.
The index-k derivative field of phi, i.e. its (k+1)-st classical derivative valued in
IteratedGradient E k, as an Lᵖ(Ω) class.
Equations
Instances For
At index zero, the iterated-gradient Lᵖ class is the existing gradient class.
Consecutive iterated-gradient fields of a test function satisfy the weak derivative identity.
Test functions inside arbitrary-order Sobolev spaces #
The linear embedding of test functions into W^{k,p}(Ω).
Equations
- TauCeti.Wkp.ofTestFunctionₗ k = { toFun := TauCeti.Wkp.ofTestFunction✝ k, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The value component of an embedded test function is its Lᵖ class.
The highest iterated-gradient component of an embedded test function is its classical
iterated gradient as an Lᵖ class.
Forgetting the highest derivative of an embedded test function gives its embedding at the
preceding order. This is intentionally not a simp lemma: the dependent index prevents the rule
from matching during simplification, which simpNF reports as a rule that will never apply.
The test-function embedding into W^{k,p}(Ω) is injective.
At order one, the arbitrary-order test-function embedding is the existing embedding into
W^{1,p}(Ω).
The spaces W^{k,p}_0(Ω) #
The closed subspace W^{k,p}_0(Ω) of W^{k,p}(Ω): the closure of the test functions
C_c^∞(Ω) in the iterated graph norm.
Equations
- TauCeti.wkp0Submodule mu Omega p k = (TauCeti.Wkp.ofTestFunctionₗ k).range.closure
Instances For
W^{k,p}_0(Ω) is the closure of the set of test-function jets.
A test function, viewed in W^{k,p}(Ω), lies in W^{k,p}_0(Ω).
A closed set containing every test-function jet contains all of W^{k,p}_0(Ω).
At order one, the arbitrary-order zero-boundary subspace is the existing
TauCeti.w1p0Submodule.
The Sobolev space W^{k,p}_0(Ω), the closure of C_c^∞(Ω) in W^{k,p}(Ω).
Equations
- TauCeti.Wkp0 mu Omega p k = ↑(TauCeti.wkp0Submodule mu Omega p k)
Instances For
The linear inclusion of test functions into the zero-boundary Sobolev space.
Equations
- TauCeti.Wkp0.ofTestFunctionₗ k = LinearMap.codRestrict (↑(TauCeti.wkp0Submodule mu Omega p k)) (TauCeti.Wkp.ofTestFunctionₗ k) ⋯
Instances For
Forgetting the zero-boundary condition recovers the usual test-function embedding.
Test functions are dense in the zero-boundary Sobolev space at every order.
Forgetting the highest derivative preserves the zero-boundary condition.
The continuous lower-order projection on zero-boundary Sobolev spaces.
Equations
- TauCeti.Wkp0.lowerOrderL k = (TauCeti.Wkp.lowerOrderL k ∘SL (↑(TauCeti.wkp0Submodule mu Omega p (k + 1))).subtypeL).codRestrict ↑(TauCeti.wkp0Submodule mu Omega p k) ⋯
Instances For
The zero-boundary lower-order projection is the usual Sobolev projection.
Forgetting the highest derivative of a zero-boundary test function gives its embedding at the preceding order.
W^{k,p}_0(Ω) is complete in the iterated graph norm.