How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Integer-order Sobolev spaces and their norms
Sources
- Juha Kinnunen, Sobolev Spaces, Chapter 1 §1.2, Definition 1.8 and the accompanying norm and local-space conventions, printed pp. 4–5. The source gives the finite- sum, the sum and its equivalent maximum, and the convention . Its printed description of says that is compactly contained; this item uses the standard explicit form that is open and is compact in .
- John K. Hunter, Notes on Partial Differential Equations, Chapter 3, §§3.1–3.5, for the Sobolev-space conventions recorded in PDE-11.
Definition
Assume Countable Choice. Let be open with , , , and . Write This is a finite nonempty set: every coordinate of such an lies in , and it contains the zero multi-index.
The real and complex classes use the conventions in The space as the quotient by null functions and Complex Lp classes and Euclidean test-function conventions. Their quotient norm values are supplied by The norm descends to the quotient and makes a normed space for for real scalars and Complex Holder, Minkowski, and the quotient norm for complex scalars.
Define to be the set of classes such that, for every , there is an class with a locally integrable representative satisfying Here the weak derivative is the one in Weak derivative of a locally integrable function. Under The Axiom of Countable Choice (), local integrability of representatives and invariance under null-set changes follow from Weak differentiation ignores null-set changes, while Uniqueness of a weak derivative as an almost-everywhere class gives uniqueness of each locally integrable derivative class. Thus this condition is a condition on the class , and each resulting derivative determines one class, denoted . The test pairing is bilinear, without conjugation.
For the zero multi-index, set . Since , The Sobolev norm expression is The formula is finite because each derivative class belongs to and is finite; at it reduces to the norm expression. The finite maximum is defined because is nonempty. The norm axioms for this expression are a separate assertion from this definition.
For open with compact and contained in , the notation means that the restriction of the class belongs to for every such .
If , the space and every space contain only the zero class, and the displayed norm expression is zero.
Definition references
The space as the quotient by null functions
Complex Lp classes and Euclidean test-function conventions
The norm descends to the quotient and makes a normed space for
Complex Holder, Minkowski, and the quotient norm
Weak derivative of a locally integrable function
The Axiom of Countable Choice ()
Weak differentiation ignores null-set changes
Uniqueness of a weak derivative as an almost-everywhere class
Depends on
- Weak derivative of a locally integrable function
- Weak differentiation ignores null-set changes
- Uniqueness of a weak derivative as an almost-everywhere class
- The space $L^p(\mu)$ as the quotient by null functions
- Complex Lp classes and Euclidean test-function conventions
- The $L^p$ norm descends to the quotient and makes $L^p$ a normed space for $1 \le p \le \infty$
- Complex Holder, Minkowski, and the quotient norm
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- A global H² bound for the Poisson adjoint on a C² domain Corollary
- A midpoint-quadrature P1 solve has an explicit Strang error budget Corollary
- A positive reaction term restores coercivity without Poincar'e Corollary
- A sufficiently large shift is coercive Corollary
- Compactly supported smooth functions are dense in W^k,p(Rⁿ) Corollary
- Injectivity removes the Lᵖ term from the global W^2,p estimate Corollary
- One-dimensional W^1,p functions have unique absolutely continuous representatives Corollary
- Poincare-Wirtinger on bounded convex domains by the direct pairwise argument Corollary
- Positive, negative, and truncated Sobolev functions Corollary
- Primal H¹ approximation on shape-regular affine finite-element meshes Corollary
- Shape-regular affine finite elements supply the Strang approximation term Corollary
- Sobolev maxima and minima form a lattice Corollary
- Subcritical compactness for W^1,p₀ on arbitrary bounded open sets Corollary
- The Dirichlet Laplacian generates an analytic heat semigroup Corollary
- The h^(r+s) L² rate under primal and dual approximation Corollary
- The inhomogeneous weak Dirichlet problem by a trace lifting Corollary
- The Poincare constant is the reciprocal square root of the first Dirichlet eigenvalue Corollary
- The Sobolev inequality for zero-boundary Sobolev closures on open sets Corollary
- The Sobolev space W^k,p is an algebra above the critical index Corollary
- W^2,p regularity implies classical or H"older regularity when p is large Corollary
- Weak differentiation has a closed graph on its natural domains Corollary
- Weak solutions depend continuously on the data Corollary
- Weak well-posedness for constant divergence-free convection Corollary
- Whole-space inequalities transfer through a Sobolev extension Corollary
- A gradient-only Poincare estimate needs normalisation Counterexample
- A hypersurface jump is not W^1,p Counterexample
- A large adverse zero-order term destroys Dirichlet coercivity Counterexample
- A mild solution need not be classical Counterexample
- A nonconvex gradient energy can lose weak lower semicontinuity Counterexample
- A nonzero boundary value creates a zero-extension jump Counterexample
- A reentrant corner prevents automatic H² dual regularity Counterexample
- A step has no locally integrable weak derivative Counterexample
- A zero-boundary solution below the CR trace regularity threshold Counterexample
- Ambient-smooth density fails on a slit disc Counterexample
- An inward cusp blocks W^1,3/2 extension Counterexample
- Boundary point values are not a function of the interior Lᵖ class Counterexample
- Boundary W^2,p regularity needs more than Lipschitz boundary Counterexample
- Cantor function has singular distributional derivative Counterexample
- Critical traces fail compactness under boundary dilation Counterexample
- Elliptic eigenvalues need not be simple Counterexample
…and 302 more results.
Dependency tree · two levels
47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Juha Kinnunen, Sobolev Spaces (2026), Chapter 1 §1.2 (standard reference, not scraped)
- John K. Hunter, Notes on Partial Differential Equations (2014), Chapter 3 (standard reference, not scraped)