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.
A coercive form need not be symmetric
Statement refuted
Assume Countable Choice for the Lax--Milgram conclusion. On with the standard inner product define Then is sesquilinear in the convention of Bounded, coercive and symmetric sesquilinear forms, bounded with and coercive with , so . It is not symmetric: with , one has while . Hence the Lax--Milgram theorem The Lax--Milgram theorem applies to this nonsymmetric form, and symmetry is not needed for existence and uniqueness; the energy-minimisation corollary Symmetric Lax--Milgram is energy minimisation is the part that genuinely uses symmetry. The example is consistent with the abstract forcing remark Nonsymmetric Lax--Milgram is not a scalar minimisation principle.
Facts & Assumptions
Given: Countable Choice; the Hilbert space with the standard inner product ; the form ; and the vectors , .
Sesquilinearity in the convention linear in the first argument and conjugate-linear in the second, with boundedness and coercivity as in Bounded, coercive and symmetric sesquilinear forms (Real and complex inner-product spaces and their induced length, Hilbert space).
Scalar facts: , , ; and for vectors in , by Cauchy--Schwarz (Real and imaginary parts, complex conjugation, and modulus, Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation).
Lax--Milgram applies to bounded coercive forms and does not assume symmetry; the energy-minimisation corollary does assume it (The Lax--Milgram theorem, Symmetric Lax--Milgram is energy minimisation, Nonsymmetric Lax--Milgram is not a scalar minimisation principle).
Proof
Sesquilinearity, boundedness and coercivity: for scalars , and directly from the definition, so is sesquilinear in the stated convention. Moreover , and Cauchy--Schwarz applied to the pairs , gives ; and has real part at least , using . Thus is coercive with constant .
Nonsymmetry: for the standard basis vectors, while , so and is not symmetric.
Consequences: is bounded and coercive but not symmetric, so Lax--Milgram applies and gives existence and uniqueness of solutions for every bounded conjugate-linear datum, while the energy-minimisation characterisation, which requires symmetry, does not apply. Thus symmetry is not needed for solvability but is genuinely used by the variational principle.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Symmetric Lax--Milgram is energy minimisation
- Bounded, coercive and symmetric sesquilinear forms
- Real and imaginary parts, complex conjugation, and modulus
- Hilbert space
- Real and complex inner-product spaces and their induced length
- Nonsymmetric Lax--Milgram is not a scalar minimisation principle
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
- The Lax--Milgram theorem
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
45 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
- Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (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)
- Gerald Teschl, Partial Differential Equations: From Classical to Modern (archived 2025 author manuscript) (standard reference, not scraped)