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.
Interior regularity for divergence-form equations
Statement
Assume Countable Choice. Let be open, , , let be as in Uniformly elliptic divergence-form operators and their sesquilinear forms with constants and with satisfying , and let . If is a local weak solution of on (Local weak solutions of a divergence-form operator), then , and for all open sets there is with Consequently the equation holds pointwise almost everywhere with understood through the a.e. defined product , and the same estimate holds for complex-valued by taking real parts in the coercive energy bounds; no splitting of complex coefficients into real and imaginary equations is used. The scaffold wrote on the right-hand side, which is ill-posed for a datum known only to lie in (for instance on is locally but not globally square-integrable); the nested formulation above is the well-posed local statement, and the quantitative content is otherwise unchanged.
Facts & Assumptions
Given: Countable Choice; the open set ; coefficients with and the bounds and ellipticity of ; the datum ; and a local weak solution of .
Local weak solution: for every . (Local weak solutions of a divergence-form operator)
Coefficient package: , , , almost everywhere, and . (Uniformly elliptic divergence-form operators and their sesquilinear forms)
Localised difference-quotient pairing. Choose nested open sets and with on . For sufficiently small and a coordinate , the test belongs to , and the local weak identity extends to it by density. Discrete integration by parts in the principal part gives , where and for . The remainder contains only cutoff terms and first difference quotients of ; since , , and for every , , uniformly in small . Furthermore, by and the product rule. Therefore the lower-order and source pairings, estimated without differencing or , satisfy . (Local weak solutions of a divergence-form operator, The difference-quotient test function and its commutators, Young's inequality for conjugate real exponents, Holder's inequality for integrals, including the endpoint cases)
Local Caccioppoli control on nested bounded sets. If is bounded with , cover by finitely many inner balls whose concentric outer balls are compactly contained in . Applying the ball Caccioppoli estimate on each pair and summing gives , with allowed to depend on the finite cover, hence on , as well as (Scaled Caccioppoli inequality on concentric balls).
Difference-quotient characterisation of , : for and , and conversely a uniform bound for implies with . (The difference-quotient characterisation of for , Uniformly bounded difference quotients represent a weak derivative).
Young and Cauchy--Schwarz inequalities with a free . (Young's inequality for conjugate real exponents, Holder's inequality for integrals, including the endpoint cases)
If satisfies for every , then ; more generally is dense in . (Smooth compactly supported functions of an open set are dense in )
Proof
Nested localization. Fix and choose . Take equal to one on . For each coordinate and sufficiently small , the test class is supported in and belongs to ; the weak identity extends from smooth tests to by density, since the form is bounded and .
Principal and lower-order terms. Write the principal pairing as as in [F3]. The weak equation gives , so taking real parts and using [F3] bounds the right side directly, without differentiating or . Choosing small relative to and absorbing the error terms into gives with , uniformly in sufficiently small . This estimate uses derivatives only of the principal coefficients; enter without being differentiated. Young's inequality and Cauchy--Schwarz [F6] absorb the energy errors.
Removing the intermediate gradient. The Caccioppoli estimate [F4] applied to gives . Substitution into step 1.2 yields uniformly in .
Recovering all second derivatives. Since on and , step 2.1 bounds uniformly for every . Applying the directional weak-limit criterion cited in [F5] with any positive threshold below the actual cutoff-support margin gives with the same bound. Summing over proves and .
The strong form and the equation a.e. On , by step 3.1, so the proved multiplier rule of The cutoff difference-quotient commutator estimate gives with weak derivative . For every , integration by parts in [F1] gives . The bracket lies in , so it vanishes a.e. there by [F7]; as the pair was arbitrary, the equation holds pointwise almost everywhere on with read as the a.e. product .
Conclusion. Every that solves locally with uniformly elliptic, and lies in with the nested-domain estimate displayed in the Statement. The argument applies directly to complex-valued data and solutions by taking real parts in the coercive energy estimates, as in step 1.2.
Source notes
Hunter's Theorem 4.27 (printed pp. 112-113) assumes principal coefficients and proves interior regularity by difference quotients. The local proof above supplies the version and permits bounded lower-order coefficients. Laugesen's Theorem 5.6 (printed pp. 108-110) gives the constant-coefficient core. The scaffold's right-hand side is not defined for when is unbounded or when blows up at a boundary point, as on shows; the repaired statement uses the standard nested domains , matching the hypothesis and the estimates actually proved.
Depends on
- Local weak solutions of a divergence-form operator
- Uniformly elliptic divergence-form operators and their sesquilinear forms
- The difference-quotient test function and its commutators
- The difference-quotient characterisation of $W^{1,p}$ for $1<p<\infty$
- Absorption of lower-order Sobolev terms in the elliptic estimate
- Scaled Caccioppoli inequality on concentric balls
- Smooth compactly supported functions of an open set are dense in $L^2$
- Young's inequality for conjugate real exponents
- Holder's inequality for integrals, including the endpoint cases
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The cutoff difference-quotient commutator estimate
- Uniformly bounded difference quotients represent a weak derivative
- A Euclidean bump for a compact set inside an open set
Used by
- Smooth data give smooth interior solutions Corollary
- Bounded discontinuous elliptic coefficients need not give H² solutions Counterexample
- Interior regularity does not imply boundary regularity Counterexample
- A piecewise-smooth coefficient gives an H² solution that is not twice classically differentiable Example
- Bootstrapping a smooth Poisson problem Example
- Poisson's equation with L² data gains two interior derivatives Example
- A finite partition glues the local interior and boundary H² estimates Lemma
- Nested-domain induction for interior elliptic derivatives Lemma
- Global H² Dirichlet regularity Theorem
- Interior Hᵏ⁺² elliptic regularity Theorem
Dependency tree · two levels
87 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
- John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter graduate notes) (standard reference, not scraped)
- Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)