TheoremStatement: Literature-sourcedProof: 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.

The Rayleigh principle for the first Dirichlet eigenvalue

Statement

Assume the Axiom of Choice and Countable Choice. In the symmetric case of The $L^{2}$ operator associated with a symmetric elliptic form with $Ω$ nonempty bounded open, let ${λ_{j}}$ be the eigenvalues of Discrete spectrum of a symmetric elliptic Dirichlet operator. Then $λ_{1} = \min_{u \in H_{0}^{1} (Ω) ∖ {0}} \frac{a (u, u)}{∥ u ∥_{L^{2}}^{2}},$ the minimum is attained exactly at the nonzero elements of the eigenspace $E_{λ_{1}}$ , and $λ_{1}$ is the smallest weak eigenvalue. If in addition the form $a$ is coercive on $H_{0}^{1} (Ω)$ with constant $α^{'} > 0$ (for instance when the hypotheses of Lax--Milgram solvability for coercive divergence-form equations hold, or $a$ is the principal Dirichlet form), then $λ_{1} \geq α^{'} > 0$ ; in general only $λ_{1} > - μ$ and the Garding bound $λ_{1} \geq - β$ are asserted.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; a nonempty bounded open set $Ω \subseteq R^{n}$ ; the symmetric divergence-form case with form $a$ ; the eigenbasis ${e_{j}}$ and nondecreasing eigenvalue list $λ_{j} \to + \infty$ of the discrete spectral theorem; and $u \in H_{0}^{1} (Ω) ∖ {0}$ .

[F1]

Eigenbasis expansion: $a (u, u) = \sum_{j} λ_{j} ∣ (u, e_{j})_{L^{2}} ∣^{2}$ absolutely convergent and $∥ u ∥_{L^{2}}^{2} = \sum_{j} ∣ (u, e_{j})_{L^{2}} ∣^{2}$ for every $u \in H_{0}^{1} (Ω)$ ; each $e_{j}$ is a weak eigenfunction with eigenvalue $λ_{j}$ (Eigenbasis expansion in the form norm, Discrete spectrum of a symmetric elliptic Dirichlet operator, Symmetric elliptic weak eigenpairs).

[F2]

The list is nondecreasing with $λ_{j} \to + \infty$ , the eigenvalue $0$ is not in the list unless it is an eigenvalue, and $λ_{1}$ is the smallest weak eigenvalue; the nonzero elements $E_{λ_{1}} ∖ {0}$ are exactly the weak eigenfunctions for $λ_{1}$ (Discrete spectrum of a symmetric elliptic Dirichlet operator).

[F3]

Coercivity: if $a (u, u) \geq α^{'} ∥ u ∥_{H_{0}^{1}}^{2}$ for all $u$ , then in particular $a (u, u) \geq α^{'} ∥ u ∥_{L^{2}}^{2}$ , and $λ_{1} \geq α^{'} > 0$ whenever the quotient is bounded below by $α^{'}$ (Bounded, coercive and symmetric sesquilinear forms, Lax--Milgram solvability for coercive divergence-form equations, The space $L^{p} (μ)$ as the quotient by null functions).

Proof

technique · direct

1.1F1F2givenalgebra

Weighted average. Let $u \in H_{0}^{1} (Ω) ∖ {0}$ and put $c_{j} : = (u, e_{j})_{L^{2}}$ . By [F1], $\sum_{j} ∣ c_{j} ∣^{2} = ∥ u ∥_{L^{2}}^{2} > 0$ and $a (u, u) = \sum_{j} λ_{j} ∣ c_{j} ∣^{2}$ , so $\frac{a (u, u)}{∥ u ∥_{L^{2}}^{2}} = \frac{\sum_{j} λ_{j} ∣ c_{j} ∣^{2}}{\sum_{j} ∣ c_{j} ∣^{2}} .$ Since $λ_{j} \geq λ_{1}$ for every $j$ by [F2], the quotient is at least $λ_{1}$ , with equality if and only if $c_{j} = 0$ for every $j$ with $λ_{j} > λ_{1}$ ; that is, if and only if $u$ lies in the closed span of the $e_{j}$ with $λ_{j} = λ_{1}$ , which is exactly $E_{λ_{1}}$ .

2.1F1F2step 1.1given

Attainment. The vector $e_{1}$ is a nonzero weak eigenfunction with $a (e_{1}, e_{1}) = λ_{1} ∥ e_{1} ∥_{L^{2}}^{2}$ and $∥ e_{1} ∥_{L^{2}} = 1$ , so the quotient at $u = e_{1}$ equals $λ_{1}$ ; combined with step 1.1, the infimum is the minimum $λ_{1}$ , attained exactly on $E_{λ_{1}} ∖ {0}$ , and $λ_{1}$ is the smallest weak eigenvalue by [F2].

3.1F3step 2.1givenalgebra∎

Lower bounds. If $a$ is coercive with constant $α^{'} > 0$ then [F3] gives $a (u, u) / ∥ u ∥_{L^{2}}^{2} \geq α^{'}$ for every nonzero $u$ , hence $λ_{1} \geq α^{'} > 0$ by step 2.1. In the general case only the bounds $λ_{1} > - μ$ and $λ_{1} \geq - β$ of the discrete spectral theorem and Garding's inequality are asserted.

Depends on

Used by

Dependency tree · two levels

59 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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, complete 392 pages) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)