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.
Bounded, coercive and symmetric sesquilinear forms
Definition
Let be a real or complex Hilbert space over with inner product linear in the first argument and conjugate-linear in the second (Real and complex inner-product spaces and their induced length, Hilbert space), and let be sesquilinear in the sense of Sesquilinear and Hermitian forms over a field with an involution, using the convention linear in the first variable: linear in the first argument and conjugate-linear in the second. The form is bounded with bound when and coercive with constant when It is symmetric (Hermitian) when for all , over this is equivalent to for every . Indeed, writing , sesquilinearity gives , and real diagonal values make this identity conjugate-symmetric. Over , symmetry means ; real diagonal values alone do not imply symmetry. The adjoint form is , and . Real bilinear convention. When is a real Hilbert space the same definitions apply with bilinear and coercive in the form ; the conjugation in the second slot is then the identity. More generally, a real bilinear form may satisfy the boundedness and coercivity conditions without being symmetric; symmetry is an additional property, not part of either condition. When every form is bounded with bound and coercive with every ; this degenerate case is kept but is never load-bearing. All constants below are named and never silently improved. No choice principle is used in this definition.
Depends on
Real and imaginary parts, complex conjugation, and modulus
Hilbert space
Linear map between vector spaces over the same field
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
Real and complex inner-product spaces and their induced length
Sesquilinear and Hermitian forms over a field with an involution, using the convention linear in the first variable
Dependency tree · 2 levels
Sources
- 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)
- John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes)