ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Dirichlet Laplacian eigenpairs on an interval

Example

Assume the Axiom of Choice and Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the discrete-spectrum and Rayleigh-principle assertions. On $(0, π)$ , for each integer $k \geq 1$ , $u_{k} (x) = \sin (k x)$ belongs to $H_{0}^{1} (0, π)$ and is a weak Dirichlet eigenfunction of the positive Laplacian $- d^{2} / d x^{2}$ with eigenvalue $k^{2}$ : $\int_{0}^{π} u_{k}^{'} (x) \overline{v^{'} (x)} d x = k^{2} \int_{0}^{π} u_{k} (x) \overline{v (x)} d x for every v \in H_{0}^{1} (0, π) .$ The functions $\sin (k x)$ are pairwise $L^{2}$ -orthogonal and have squared norm $π / 2$ ; hence the displayed pairs are eigenpairs with pairwise distinct eigenvalues. The Rayleigh principle gives $λ_{1} \leq 1$ , witnessed by $(\sin x, 1)$ , where $λ_{1}$ is the first eigenvalue in Discrete spectrum of a symmetric elliptic Dirichlet operator and the variational characterization is The Rayleigh principle for the first Dirichlet eigenvalue. Neither completeness of ${\sin (k x)}$ , nor simplicity of the individual eigenvalues, nor the sharp Poincare constant is asserted here.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; the interval $(0, π)$ ; an integer $k \geq 1$ ; and $u_{k} (x) = \sin (k x)$ .

[F1]

Coefficient convention: with $n = 1$ , $a^{11} = 1$ , $b = c = 0$ the divergence-form operator is the positive Laplacian and its form is $a (u, v) = \int_{0}^{π} u^{'} \overline{v^{'}} d x$ (Uniformly elliptic divergence-form operators and their sesquilinear forms, Symmetric elliptic weak eigenpairs).

[F2]

Sobolev conventions: $H_{0}^{1} (0, π)$ is the closure of $C_{c}^{\infty} (0, π)$ in the norm $∥ w ∥_{H^{1}}^{2} = ∥ w ∥_{L^{2}}^{2} + ∥ w^{'} ∥_{L^{2}}^{2}$ , and classical derivatives of smooth functions are weak derivatives (Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms, Classical derivatives agree with weak derivatives).

[F3]

Cutoffs: the standard smooth step $σ$ of The standard smooth step function gives $χ (s) = σ (s - 1)$ , zero for $s \leq 1$ and one for $s \geq 2$ . Its derivative is bounded, being continuous and supported in $[1, 2]$ , by A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value; set $η_{ε} (x) = χ (x / ε) χ ((π - x) / ε)$ . Then $∣ η_{ε}^{'} ∣ \leq C / ε$ , and it has the strip properties used below. The chain rule and sine derivatives are The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ and The derivatives of sine and cosine are cosine and minus sine, and integer shifts give $\sin (k π) = 0$ by Quarter-turn values and shifts by pi/2 and pi.

[F4]

Calculus: the second fundamental theorem and the addition formulas give $\int_{a}^{b} g^{'} = g (b) - g (a)$ for $C^{1}$ functions and $2 \sin (m x) \sin (n x) = \cos ((m - n) x) - \cos ((m + n) x)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The addition formulas for sine and cosine).

Verification

technique · direct

1.1F2F3F4givenalgebra

Membership in $H_{0}^{1}$ . By [F2] and [F3], $u_{k}^{'} = k \cos (k x)$ and $u_{k}^{''} = - k^{2} u_{k}$ are weak derivatives. For $0 < ε < π / 4$ use the cutoff $η_{ε}$ of [F3]; then $η_{ε} u_{k} \in C_{c}^{\infty} (0, π)$ . On the boundary strips $A_{ε} = (0, 2 ε) \cup (π - 2 ε, π)$ , $∣ u_{k} ∣ \leq k dist (x, {0, π}) \leq 2 k ε$ by integration of $u_{k}^{'}$ from the nearest endpoint, and $∣ u_{k}^{'} ∣ \leq k$ . Since $(η_{ε} u_{k} - u_{k})^{'} = (η_{ε} - 1) u_{k}^{'} + η_{ε}^{'} u_{k}$ , $∥ η_{ε} u_{k} - u_{k} ∥_{H^{1}}^{2} \leq \int_{A_{ε}} (∣ u_{k} ∣^{2} + 2 ∣ u_{k}^{'} ∣^{2} + 2 ∣ η_{ε}^{'} ∣^{2} ∣ u_{k} ∣^{2}) \leq 4 ε (4 k^{2} ε^{2} + 2 k^{2} + 8 C^{2} k^{2}) ⟶ 0.$ Thus $u_{k} \in H_{0}^{1}$ by the closure definition.

1.2F1F2givenalgebra

The weak eigenidentity. Let $v \in H_{0}^{1} (0, π)$ and choose $v_{j} \in C_{c}^{\infty} (0, π)$ with $v_{j} \to v$ in $H^{1}$ (possible by [F2]). For each $j$ , integration by parts on the compact support of $v_{j}$ has no boundary term and gives, since $u_{k}^{''} = - k^{2} u_{k}$ , $\int_{0}^{π} u_{k}^{'} \overline{v_{j}^{'}} = - \int_{0}^{π} u_{k}^{''} \overline{v_{j}} = k^{2} \int_{0}^{π} u_{k} \overline{v_{j}}$ ; the left side differs from $\int u_{k}^{'} \overline{v^{'}}$ by at most $∥ u_{k}^{'} ∥_{L^{2}} ∥ v_{j}^{'} - v^{'} ∥_{L^{2}}$ , and the right side from $k^{2} \int u_{k} \overline{v}$ by at most $k^{2} ∥ u_{k} ∥_{L^{2}} ∥ v_{j} - v ∥_{L^{2}}$ , so passing to the limit gives the displayed identity; by [F1] and the weak eigenpair definition, $(k^{2}, u_{k})$ is a Dirichlet eigenpair (Symmetric elliptic weak eigenpairs).

1.3F4givenalgebra

Orthogonality and norms. For integers $m, n \geq 1$ the addition formula [F4] gives $2 \sin (m x) \sin (n x) = \cos ((m - n) x) - \cos ((m + n) x)$ ; integrating over $(0, π)$ with the second fundamental theorem gives $0$ when $m \neq n$ (both cosine integrals vanish) and $\int_{0}^{π} \sin^{2} (n x) d x = \frac{1}{2} \int_{0}^{π} (1 - \cos (2 n x)) d x = π / 2$ . Hence the $u_{k}$ are pairwise $L^{2}$ -orthogonal with squared norm $π / 2$ , and the eigenvalues $k^{2}$ are pairwise distinct.

2.1F1F4step 1.2step 1.3givenalgebra∎

The Rayleigh bound. By step 1.2 applied with $k = 1$ , $u_{1} = \sin x$ is a weak eigenfunction with eigenvalue $1$ ; the Rayleigh principle The Rayleigh principle for the first Dirichlet eigenvalue then gives $λ_{1} \leq 1$ , since the Rayleigh quotient of $\sin x$ equals $∥ u_{1}^{'} ∥_{L^{2}}^{2} / ∥ u_{1} ∥_{L^{2}}^{2} = \int_{0}^{π} \cos^{2} x d x / \int_{0}^{π} \sin^{2} x d x = 1$ by [F4] and step 1.3. No completeness of the family ${\sin (k x)}$ , no simplicity of the eigenvalues and no sharp Poincare constant is asserted.

Depends on

Used by

Elliptic eigenvalues need not be simple Counterexample
Elliptic Fredholm solvability can fail at an eigenvalue Counterexample
A shift removes a negative zero-order obstruction Example
The Neumann Laplacian has a zero constant mode Example

Dependency tree · two levels

100 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

Richard S. Laugesen, Spectral Theory of Partial Differential Equations (University of Illinois lecture notes, arXiv:1203.2344, complete 120 pages) (standard reference, not scraped)
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)