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.
Uniformly elliptic divergence-form operators and their sesquilinear forms
Definition
Assume Countable Choice for the Sobolev interfaces. Let be open, , and let . Let , , be measurable (A measurable function between measurable spaces) and essentially bounded (The space of essentially bounded measurable functions, The essential supremum of a measurable function with respect to a measure), with bounds and suppose the uniform ellipticity condition holds: there is with The associated divergence-form expression is (Einstein summation over ), and the associated sesquilinear form on is The form is linear in and conjugate-linear in , in the convention of Bounded, coercive and symmetric sesquilinear forms; the classical Dirichlet problem consists of in with prescribed boundary values. The operator is determined by the coefficient functions only a.e., and all later statements about are statements about those classes. Where the domain and boundary data demand it (Weak Dirichlet solutions for a divergence-form operator, The inhomogeneous weak Dirichlet problem by a trace lifting) the domain is additionally a bounded domain (Bounded C^k domains and boundary charts). The convention is the complex sesquilinear one with conjugation in the second slot, as the plan's convention audit directs; the real case is the same with conjugation read as the identity.
Depends on
Bounded C^k domains and boundary charts
Real and imaginary parts, complex conjugation, and modulus
Complex Lp classes and Euclidean test-function conventions
The Axiom of Countable Choice ()
The essential supremum of a measurable function with respect to a measure
The notation and the reserved zero-boundary symbol
The space of essentially bounded measurable functions
A measurable function between measurable spaces
Integer-order Sobolev spaces and their norms
Weak derivative of a locally integrable function
Dependency tree · 2 levels
Sources
- John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes)
- Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes)
- Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan)
- Gerald Teschl, Partial Differential Equations: From Classical to Modern (archived 2025 author manuscript)