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 conforming P1 Dirichlet discretization gives a first Ritz upper bound
Example
Let and put in counterclockwise order; these divide each side into two boundary edges. Let . The eight triangles , with indices modulo , form a matching affine triangulation. Let be the continuous piecewise-linear hat with value at and value at each . Its trace vanishes on the boundary. The one-dimensional conforming Ritz space has first Ritz value ; hence the exact Dirichlet ground-state eigenvalue satisfies .
Facts & Assumptions
Given: Countable Choice and the Axiom of Choice; the square, the eight triangles, the hat function , and the Dirichlet Laplacian forms and .
Matching continuous piecewise polynomials with zero boundary facet trace lie in (Matching affine simplicial meshes and shape regularity, Broken and conforming polynomial spaces on a matching mesh, Zero-boundary conforming polynomials lie in W0 1p and satisfy Poincare).
The exact symmetric Dirichlet spectrum has a nondecreasing eigenvalue list, and its first eigenvalue is the attained minimum of the Rayleigh quotient (the Courant–Fischer theorem assumes both Choice and Countable Choice) (Discrete spectrum of a symmetric elliptic Dirichlet operator, The Courant-Fischer min-max principle for elliptic eigenvalues).
Proof
Given: The conforming mesh, nodal hat , and the continuous and discrete Dirichlet Rayleigh quotients.
Adjacent triangles share the same endpoint values of , so their linear traces agree on each interior edge. The boundary edges have zero values at both endpoints, so their linear traces vanish identically. Thus [F1] places in . It is nonzero because . Each triangle has base length , height and area ; the hat changes from at to across height , so on each cell. Therefore
On a triangle, is the barycentric coordinate of . On the reference triangle , direct integration gives An affine change of variables preserves the ratio of this integral to the triangle area, so . Summing the eight cells gives .
Because is one-dimensional, its sole Ritz value is its Rayleigh quotient, . By [F2], the continuous first eigenvalue minimizes the same quotient over all nonzero functions. Since is an admissible nonzero function by step 1.1, .
Remarks
This exact calculation verifies the fixed-index conforming upper bound for one mesh. It does not check the small best-approximation-gap premise needed for the quadratic error estimate on this particular coarse space.
Depends on
- The Axiom of Choice
- Broken and conforming polynomial spaces on a matching mesh
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Matching affine simplicial meshes and shape regularity
- The Courant-Fischer min-max principle for elliptic eigenvalues
- Discrete spectrum of a symmetric elliptic Dirichlet operator
- Zero-boundary conforming polynomials lie in W0 1p and satisfy Poincare
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
- Jean-Luc Guermond, MATH 661 Finite Element Methods, Fall 2025, Chapter 47 (standard reference, not scraped)
- Bertrand Mercier, Topics in Finite Element Solution of Elliptic Problems, Chapter 8 (standard reference, not scraped)