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.
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
- One-dimensional W^1,p functions have unique absolutely continuous representatives Corollary
- Positive, negative, and truncated Sobolev functions Corollary
- Sobolev maxima and minima form a lattice Corollary
- Weak differentiation has a closed graph on its natural domains Corollary
- A hypersurface jump is not W^1,p Counterexample
- A step has no locally integrable weak derivative Counterexample
- Cantor function has singular distributional derivative Counterexample
- Lp and Sobolev classes do not determine point values Counterexample
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- Subcritical W^1,p is not closed under multiplication Counterexample
- Absolute continuity on almost every coordinate line Definition
- The notation Hᵏ and the reserved zero-boundary symbol Definition
- A clipped affine function keeps its zero region Example
- Absolute value has a Dirac second derivative Example
- Matching C¹ pieces across a hyperplane have no jump derivative Example
- Sharp Sobolev threshold for a radial power Example
- The absolute value has a weak first derivative Example
- Bounded restriction and cutoff localisation in Sobolev spaces Lemma
- Integration by parts for dual-exponent Sobolev functions Lemma
- Sobolev functions paste across an overlap Lemma
- The Sobolev norm descends to equivalence classes Lemma
- Weak derivatives persist under local Lp limits Lemma
- Weak Leibniz rule with a smooth factor Lemma
- Weak lower semicontinuity of the Sobolev norm Lemma
- Chain rule for a C¹ function with bounded derivative Theorem
- Chain rule for globally Lipschitz scalar maps of Sobolev functions Theorem
- Hᵏ is a Hilbert space under the derivative-sum inner product Theorem
- Integer-order Sobolev spaces are Banach Theorem
- Integer-order W^k,2 and Hᵏ agree with equivalent norms Theorem
- The ACL characterisation of W^1,p Theorem
- Zero weak gradient gives componentwise constants Theorem
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)