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.
The Sobolev inequality for zero-boundary Sobolev closures on open sets
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be open, , and . There is with for every .
Facts & Assumptions
Given: The Axiom of Choice; an open set ; ; ; a field ; and a class .
is the closure of in the norm, and its elements are classes with weak gradients in (Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms).
Extension by zero sends into , the weak derivatives of the extension are the zero extensions of the weak derivatives, and all component norms are preserved (Zero extension of W_0^{1,p} has no boundary derivative).
For , the whole-space inequality holds for every (The Gagliardo-Nirenberg-Sobolev inequality for ). For it holds for (The p=1 Gagliardo-Nirenberg-Sobolev inequality). Here (The Sobolev conjugate exponent and the scaling identity).
Every space for is complete and norm convergence has an almost-everywhere convergent subsequence (Riesz-Fischer completeness of for , Complex Lp completeness and almost-everywhere subsequences).
Proof
Zero extension. Let be the extension of by zero. By [F2], , its weak gradient is the zero extension of , and , componentwise.
For , apply [F3] to and use step 1.1. For , choose converging to in by [F1]; their zero extensions converge to in by [F2]. The endpoint estimate [F3] applied to differences shows that these extensions are Cauchy in . By [F4] their limit in that space exists; an almost-everywhere subsequence, followed by an almost-everywhere subsequence, identifies it with . Passing to the limit in the endpoint estimate gives . Step 1.1 transfers both cases to , proving the assertion.
Source notes
The corollary is the zero-trace case of the whole-space Sobolev inequality, Kinnunen's Remark 3.4(3) and Laugesen's Theorem 3.18: the extension by zero has the same weak gradient up to the boundary of , so the whole-space result transfers verbatim. At the smooth endpoint estimate is extended by the closure approximation and completeness.
Depends on
The Axiom of Choice
The Sobolev conjugate exponent and the scaling identity
Zero-boundary Sobolev space as a norm closure
Integer-order Sobolev spaces and their norms
The space as the quotient by null functions
Zero extension of W_0^{1,p} has no boundary derivative
The Gagliardo-Nirenberg-Sobolev inequality for
The p=1 Gagliardo-Nirenberg-Sobolev inequality
Riesz-Fischer completeness of for
Complex Lp completeness and almost-everywhere subsequences