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 norm of W^{1,p}(Ω) is that of TauCeti.W1p: the Lᵖ norm of the pointwise Euclidean norm of the value and the gradient. Each later stage takes the Euclidean product norm of its two components, so at every order k + 2 and for every p the squared norm is the sum of the squared norm of the one-order-lower component and the squared norm of the highest weak derivative. At order one this identity holds for p = 2 but not in general; it fails, for instance, for sin in W^{1,∞}(ℝ). The derivative fields above first order carry operator norms, so the norm of W^{k,2}(Ω) with k ≥ 2 need not be induced by an inner product: on Ω = (0,1)² ⊆ ℝ², for instance, x²/2 and y²/2 violate the parallelogram law. It is a Banach-space norm, not in general the Hilbert-space norm of H^k(Ω).

Implementation notes #

The bundled stage machinery TauCeti.SobolevStage, TauCeti.firstSobolevStage, TauCeti.SobolevStage.next, and TauCeti.sobolevStage is public on purpose: it is what indexes the type TauCeti.Wkp, so its normed, complete structure and the order 0 and 1 boundary cases are recovered by unfolding it rather than by transport. TauCeti.firstSobolevStage, TauCeti.SobolevStage.next, and TauCeti.Wkp are reducible. The recursion TauCeti.sobolevStage is exposed but semireducible, so that at a concrete order instance search stops at (sobolevStage j).Space and finds the TauCeti.SobolevStage shortcut instances keyed there. 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 identifications of Wkp … 1 with TauCeti.W1p and of Wkp … (k + 2) with a TauCeti.WeakDerivStep are therefore definitional but not reducible, and rw and simp do not unfold TauCeti.sobolevStage to match across them in either direction: a lemma stated for TauCeti.W1p or TauCeti.WeakDerivStep applied to a Wkp … 1 or Wkp … (k + 2) term, and a Wkp-indexed lemma applied to a term typed as TauCeti.W1p or TauCeti.WeakDerivStep, must both be given their argument explicitly. 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.Wkp: W^{k,p}(Ω), with Wkp 0 = Lᵖ(Ω) and Wkp 1 = W1p.
TauCeti.Wkp.lowerOrder: the continuous projection W^{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 #

The iterated weak-derivative definition and closed-graph completeness argument follow L. C. Evans, Partial Differential Equations, Chapter 5, §5.2.