Arbitrary-order weak Sobolev spaces #
This file constructs the real-valued Sobolev space W^{k,p}(Ω) for every natural number
k, on an open subset of a finite-dimensional real inner product space. The first-order stage
is TauCeti.W1p. Every successor stage applies TauCeti.WeakDerivStep to the highest weak
derivative of the preceding stage. Thus an element of W^{k+1,p}(Ω) records an element of
W^{k,p}(Ω) and an Lᵖ weak derivative of its order-k derivative.
The iterated derivative fields are basis-free. TauCeti.IteratedGradient E 0 is E, the weak
gradient identified with a linear functional by the real inner product, and
TauCeti.IteratedGradient E (j+1) adds one continuous-linear derivative direction on the left.
Consequently the highest field of W^{k+1,p} has type
Lᵖ(Ω; TauCeti.IteratedGradient E k).
Every stage is a closed weak-derivative graph, hence complete. No boundedness or boundary
regularity of Ω is used. The graph norm is obtained recursively from Euclidean product norms:
at each positive order its square is the sum of the squared norm of the one-order-lower component
and the squared norm of the highest weak derivative.
Implementation notes #
The bundled stage machinery TauCeti.IteratedGradientModel, TauCeti.iteratedGradientModel,
TauCeti.SobolevStage, TauCeti.firstSobolevStage, TauCeti.SobolevStage.next, and
TauCeti.sobolevStage is public and reducible on purpose: it is what indexes the types
TauCeti.IteratedGradient and TauCeti.Wkp, so their normed, complete structures and the order
0 and 1 boundary cases are recovered by unfolding it rather than by transport. The shortcut
instances are provided at both the bundled-stage and Wkp indexings so instance search need not
rederive these structures through the recursion. The projections below are sealed instead, and
are used through their characteristic equations TauCeti.Wkp.lowerOrder_zero,
TauCeti.Wkp.lowerOrder_succ, TauCeti.Wkp.iteratedGradient_zero,
TauCeti.Wkp.iteratedGradient_succ, TauCeti.Wkp.value_zero, and
TauCeti.Wkp.value_succ.
Main declarations #
TauCeti.IteratedGradient: the basis-free target of an iterated weak derivative.TauCeti.iteratedGradientChain: the corresponding classical derivative fields of a smooth scalar function.TauCeti.Wkp:W^{k,p}(Ω), withWkp 0 = Lᵖ(Ω)andWkp 1 = W1p.TauCeti.Wkp.lowerOrder: the continuous projectionW^{k+1,p} → W^{k,p}.TauCeti.Wkp.iteratedGradient: the highest weak derivative of a positive-order Sobolev function.TauCeti.Wkp.hasWeakFDerivOn_iteratedGradient: adjacent recorded derivatives satisfy the weak derivative identity.
References #
This completes the arbitrary-order space and completeness part of Lane A.1, target 1, in
TauCetiRoadmap/PDE/README.md. The iterated weak-derivative definition and closed-graph
completeness argument follow L. C. Evans, Partial Differential Equations, Chapter 5, §5.2.
The normed-space data underlying an iterated weak gradient.
- Space : Type u
The carrier space for the iterated weak gradient.
- normedAddCommGroup : NormedAddCommGroup self.Space
The normed additive commutative group structure on
Space. - normedSpace : NormedSpace ℝ self.Space
The normed
ℝ-space structure onSpace.
Instances For
The recursively bundled target of an iterated weak gradient.
Equations
- One or more equations did not get rendered due to their size.
- TauCeti.iteratedGradientModel E 0 = { Space := E, normedAddCommGroup := inst✝¹, normedSpace := inst✝ }
Instances For
The target of an iterated weak gradient, indexed by the number of derivative directions added
beyond the gradient. At j = 0 this is the gradient vector E; each successor adds one
continuous-linear derivative direction on the left.
Equations
Instances For
The classical derivative fields of a smooth scalar function, in the basis-free
nested-linear-map types used by TauCeti.Wkp. Index zero is the gradient and each successor is
the Fréchet derivative of the preceding field.
Equations
- TauCeti.iteratedGradientChain f 0 = fun (x : F) => gradient f x
- TauCeti.iteratedGradientChain f j.succ = fderiv ℝ (TauCeti.iteratedGradientChain f j)
Instances For
Every field in the iterated-gradient chain of a smooth function is smooth.
Every field in the iterated-gradient chain of a compactly supported function has compact support.
The bundled data used to iterate weak-derivative graph spaces. Its jth stage carries the
space of order j + 1 and its highest derivative projection.
- Space : Type u
The Sobolev space of order
j + 1. - normedAddCommGroup : NormedAddCommGroup self.Space
The normed additive commutative group structure on the order-
j + 1Sobolev space. - normedSpace : NormedSpace ℝ self.Space
The normed
ℝ-space structure on the order-j + 1Sobolev space. - completeSpace : CompleteSpace self.Space
The completeness instance for the order-
j + 1Sobolev space. - iteratedGradientL : self.Space →L[ℝ] ↥(MeasureTheory.Lp (IteratedGradient E j) p (mu.restrict ↑Omega))
The continuous projection to the highest weak derivative field.
Instances For
The first stage of the arbitrary-order construction is W1p, with value and gradient as
its lower-order and highest-derivative projections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Adjoin the weak derivative of a stage's highest derivative field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The jth iterated weak-derivative stage, representing Sobolev order j + 1.
Equations
Instances For
Equations
The arbitrary-order, real-valued weak Sobolev space W^{k,p}(Ω). At order zero this is
Lᵖ(Ω); order one is W1p; every further order adjoins the weak derivative of the highest
derivative field from the preceding order.
Equations
- TauCeti.Wkp mu Omega p 0 = ↥(MeasureTheory.Lp ℝ p (mu.restrict ↑Omega))
- TauCeti.Wkp mu Omega p j.succ = (TauCeti.sobolevStage j).Space
Instances For
Every weak Sobolev space W^{k,p}(Ω) is complete in its iterated graph norm.
The continuous projection that forgets the highest weak derivative.
Equations
Instances For
A positive-order Sobolev function regarded as a Sobolev function of one lower order.
Equations
- TauCeti.Wkp.lowerOrder k u = (TauCeti.Wkp.lowerOrderL k) u
Instances For
Evaluating the continuous lower-order projection equals lowerOrder.
The continuous projection to the highest weak derivative of a positive-order Sobolev
function. For W^{k+1,p} its target is Lᵖ(Ω; IteratedGradient E k).
Equations
Instances For
The highest weak derivative recorded by a positive-order Sobolev function.
Equations
Instances For
Evaluating the continuous highest-derivative projection equals iteratedGradient.
The continuous projection of a Sobolev function to its Lᵖ value component.
Equations
- TauCeti.Wkp.valueL 0 = ContinuousLinearMap.id ℝ (TauCeti.Wkp mu Omega p 0)
- TauCeti.Wkp.valueL j.succ = TauCeti.Wkp.valueL j ∘SL TauCeti.Wkp.lowerOrderL j
Instances For
The Lᵖ value component of an arbitrary-order Sobolev function.
Equations
- TauCeti.Wkp.value k u = (TauCeti.Wkp.valueL k) u
Instances For
Taking the value component commutes with forgetting the highest derivative.
At first order, the generic lower-order projection is the W1p value projection.
At first order, the generic value projection is the W1p value projection.
At first order, the generic highest derivative is the W1p weak gradient.
The highest derivative projection is the one stored in the corresponding recursive stage.
Above first order, the lower-order projection is the preceding-component projection of the generic weak-derivative graph step.
Above first order, the highest derivative is the derivative component of the generic weak-derivative graph step.
The first weak derivative identity, with the gradient identified with a linear functional through the real inner product.
Construct an order-k+2 Sobolev function from an order-k+1 function and a weak
derivative of its highest derivative.
Equations
- TauCeti.Wkp.mk k u D h = TauCeti.WeakDerivStep.mk (TauCeti.sobolevStage k).iteratedGradientL u D h
Instances For
The highest derivative of an order-k+2 Sobolev function is the weak Fréchet derivative
of the highest derivative of its order-k+1 projection.
Two positive-order Sobolev functions are equal when their lower-order components are equal; uniqueness of weak derivatives determines the highest components.
Two arbitrary-order Sobolev functions are equal when their Lᵖ value components are equal.
Successive uniqueness of weak derivatives determines every higher component.
The graph norm controls the one-order-lower Sobolev component.
The iterated graph norm controls the Lᵖ value component at every order.
The graph norm controls the highest weak derivative.
At exponent two, the squared graph norm at every positive order is the sum of the squared norm of the lower-order component and the squared norm of the highest weak derivative.