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.
Scaled Caccioppoli inequality on concentric balls
Statement
In the setting of The Caccioppoli inequality for weak elliptic solutions, for concentric balls one has, with the explicit scale, where does not depend on or on . The displayed is the scale used in the nested-ball iteration; the constants are not asserted to be sharp, and no claim is made as .
Facts & Assumptions
Given: Countable Choice; the setting of The Caccioppoli inequality for weak elliptic solutions: an open set , a scalar field , coefficients with ellipticity constant and bounds , a class and a local weak solution of ; and concentric balls .
Caccioppoli estimate: for every ball and every there is with (The Caccioppoli inequality for weak elliptic solutions)
norms of classes are , so each integral in [F1] is the square of the corresponding norm. (The space as the quotient by null functions)
Proof
The hypotheses of [F1] are exactly those of the given setting, so [F1] provides a constant with The constant does not depend on because [F1] itself manufactures it only from .
Writing each integral as the square of the norm via [F2], the inequality of step 1.1 becomes exactly the displayed estimate: the left side is and the right side is . Nothing was changed except the notation, so the scale and the independence of the constant from hold as asserted.
Source notes
Simon's Lemma 1 (printed p. 59) records the constant for the estimate; Hunter's (4.39) (printed p. 112) uses the same scale. The zero-order term is retained explicitly because it cannot be absorbed into the term when ; it is controlled at the base of every nested-ball iteration.
Depends on
Used by
Dependency tree · two levels
33 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
- Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)
- 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)