Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-30
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-p sum, the p=∞ sum and its equivalent maximum, and the convention D0u=u. Its printed description of U⋐Ω says that U is compactly contained; this item uses the standard explicit form that U is open and U‾ 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 Ω⊆Rn be open with n≥1, k∈N0, 1≤p≤∞, and K∈{R,C}. Write Ak={α∈N0n:∣α∣≤k}. This is a finite nonempty set: every coordinate of such an α lies in {0,…,k}, and it contains the zero multi-index.

The real and complex Lp classes use the conventions in The space Lp(μ) as the quotient by null functions and Complex Lp classes and Euclidean test-function conventions. Their quotient norm values are supplied by The Lp norm descends to the quotient and makes Lp a normed space for 1≤p≤∞ for real scalars and Complex Holder, Minkowski, and the quotient norm for complex scalars.

Define Wk,p(Ω;K) to be the set of classes u∈Lp(Ω;K) such that, for every α∈Ak, there is an Lp(Ω;K) class with a locally integrable representative vα satisfying ∫Ωu Dαφ dx=(−1)∣α∣∫Ωvαφ dxfor every φ∈Cc∞(Ω). Here the weak derivative is the one in Weak derivative of a locally integrable function. Under The Axiom of Countable Choice (ACω), local integrability of Lp 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 Lp class u, and each resulting derivative determines one Lp class, denoted Dαu. The test pairing is bilinear, without conjugation.

For the zero multi-index, set D0u=u. Since A0={0}, W0,p(Ω;K)=Lp(Ω;K). The Sobolev norm expression is ∥u∥Wk,p(Ω)={(∑α∈Ak∥Dαu∥Lp(Ω)p)1/p,1≤p<∞,max⁡α∈Ak∥Dαu∥L∞(Ω),p=∞. The formula is finite because each derivative class belongs to Lp and Ak is finite; at k=0 it reduces to the Lp norm expression. The finite maximum is defined because Ak is nonempty. The norm axioms for this expression are a separate assertion from this definition.

For open U⊆Ω with U‾ compact and contained in Ω, the notation Wlock,p(Ω;K) means that the restriction of the class belongs to Wk,p(U;K) for every such U.

If Ω=∅, the Lp space and every Wk,p space contain only the zero class, and the displayed norm expression is zero.

Depends on

Used by

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