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.
Weak subsolutions and supersolutions of a divergence-form equation
Definition
Assume Countable Choice and the Axiom of Choice for the Sobolev, trace and embedding interfaces below. Let , let be open, and let and its sesquilinear form be as in Uniformly elliptic divergence-form operators and their sesquilinear forms with ellipticity constant and coefficient bounds . For the order comparison below, take real coefficients and a real-valued source (Locally integrable functions as regular distributions, The space as the quotient by null functions).
A real class (The notation and the reserved zero-boundary symbol) is a local weak subsolution of on if and a local weak supersolution if the reverse inequality holds; it is a local weak solution if equality holds for every real . These tests make every pairing finite for .
Global Sobolev-test version. If the source defines a continuous functional (The negative Sobolev space ), then a real is a global weak subsolution if with the reverse inequality defining a global weak supersolution and equality defining a global weak solution. The local and global formulations agree when both apply, by continuity of the form and and the following positive-cone density argument. Given , choose real converging to in and a subsequence converging a.e.; such a subsequence follows by choosing and applying Chebyshev and countable subadditivity to . The positive-part chain rule gives . The second term tends to zero in by dominated convergence, since its indicator converges where and a.e. where ; the first term and the function difference converge in . Thus in . Each has compact support, so zero extension followed by nonnegative unit-mass mollification with sufficiently small radius gives a nonnegative approximant within in (Positive, negative, and truncated Sobolev functions, Compactly supported Sobolev functions extend by zero in every integer order, Local smooth approximation in integer-order Sobolev spaces, Dominated convergence, Chebyshev-Markov inequality for the integral). In particular, suffices by Cauchy--Schwarz and ; on a bounded domain, with for (or for ) suffices because lies in the Sobolev range (The Sobolev inequality for zero-boundary Sobolev closures on open sets, The critical Sobolev embedding into every finite , Holder's inequality for integrals, including the endpoint cases). If , the local inequality also extends to nonnegative tests on any bounded open , since .
For complex-valued coefficients or classes, only the weak-solution identity with a specified continuous complex source functional is used; no subsolution or supersolution order is defined by comparing complex numbers. In the real setting, a weak solution is both a subsolution and a supersolution exactly when the same source functional is used in both inequalities.
Signed essential extrema. For a real measurable class on a positive-measure set , write in the extended reals, and . A finite essential supremum is itself an a.e. upper bound: take the union of the null exceptional sets for the bounds . These signed extrema differ from the essential supremum of used to define the norm. For a continuous representative on an open set, its pointwise and essential extrema agree, since a strict violation of an essential bound would hold on a nonempty open set of positive measure.
Weak boundary order (for ). Let in addition and let be a bounded domain (Bounded C^k domains and boundary charts) with trace operator (The trace operator on a bounded domain). For real and one writes on if , and on if ; by The kernel of the trace is the closure of the test functions these are respectively the statements and a.e. on , as justified by A function whose trace is at most a level has positive part in the zero-boundary space ↗, and it is independent of the chosen representatives. The boundary supremum is with ; the set is nonempty as soon as is essentially bounded above.
Conventions
- Sign convention. In the real order theory, the subsolution inequality is against nonnegative tests. For the operator , the favourable pointwise sign in the maximum principle is ; negating a supersolution preserves the same coefficients, so the same sign is favourable for the corresponding minimum estimate.
- Real order versus complex identities. The maximum-principle, De Giorgi and Harnack results use real-valued , real coefficients and real sources, so their inequalities compare real numbers. Complex local weak solutions use the compactly supported identity of Local weak solutions of a divergence-form operator; a complex global weak identity uses a specified continuous functional on . No order notion is assigned to a complex-valued form.
- No boundary condition is imposed by the subsolution or supersolution notion itself, and the boundary order is only introduced on a bounded domain, through the trace; it is never read off pointwise boundary values of a class.
Sources
- Simon, Lectures on Partial Differential Equations, Lecture 13, printed pp. 147-158: the real weak form against nonnegative , the conventions (i)-(iv) for on and , and the weak maximum principle Theorem 4. Simon works with real-valued data; the present definition records the local real order convention and the separate global extension.
- Teschl, PDE: From Classical to Modern, Chapter 10 Section 1: Theorem 10.1, Lemma 10.2 and the same boundary convention for on .
- Schikorra, Partial Differential Equations, Chapter 2 Sections II.1-II.2: Definitions II.1.1 and II.1.3, the sign convention for the zeroth-order term, and Theorem II.2.1.
Depends on
Uniformly elliptic divergence-form operators and their sesquilinear forms
Weak Dirichlet solutions for a divergence-form operator
Local weak solutions of a divergence-form operator
Zero-boundary Sobolev space as a norm closure
Integer-order Sobolev spaces and their norms
The notation and the reserved zero-boundary symbol
The space as the quotient by null functions
Complex Lp classes and Euclidean test-function conventions
Locally integrable functions as regular distributions
The trace operator on a bounded domain
The kernel of the trace is the closure of the test functions
Bounded C^k domains and boundary charts
Meyers–Serrin density on an arbitrary open set
The elliptic form is well defined and bounded on
The negative Sobolev space
The Sobolev inequality for zero-boundary Sobolev closures on open sets
The critical Sobolev embedding into every finite
Holder's inequality for integrals, including the endpoint cases
The Axiom of Countable Choice ()
The Axiom of Choice
Positive, negative, and truncated Sobolev functions
Compactly supported Sobolev functions extend by zero in every integer order
Local smooth approximation in integer-order Sobolev spaces
Dominated convergence
Chebyshev-Markov inequality for the integral
Dependency tree · 2 levels
Sources
- Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete author scan, 118 sheets reproducing the 223 printed pages of the manuscript, two logical pages per sheet)
- Gerald Teschl, Partial Differential Equations: From Classical to Modern (author manuscript, version 11 February 2025; complete 392-page archived text)
- Armin Schikorra, Partial Differential Equations (University of Pittsburgh, version 4 December 2019; complete 185-page lecture notes)