TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Higher eigenvalues by orthogonality-constrained minimisation

Statement

Assume the Axiom of Choice, the ultrafilter lemma, DC and HB (The Axiom of Choice, The ultrafilter extension principle (UL/BPI), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The real dominated-extension principle as an additional hypothesis over ZF). Let $n \geq 1$ , let $Ω \subseteq R^{n}$ be a nonempty bounded open set, let $λ_{1} \leq λ_{2} \leq \dots$ and ${e_{j}}$ be the eigenvalues and orthonormal eigenbasis of the real Dirichlet Laplacian, supplied by Discrete spectrum of a symmetric elliptic Dirichlet operator with $a_{0} (v, w) = \int_{Ω} D v \cdot D w$ (The $L^{2}$ operator associated with a symmetric elliptic form, Symmetric elliptic weak eigenpairs, The notation $H^{k}$ and the reserved zero-boundary symbol), and fix $k \geq 2$ . Put $S_{k} = {u \in H_{0}^{1} (Ω; R) : ∥ u ∥_{L^{2}} = 1, (u, e_{j})_{L^{2}} = 0 for j < k}$ and $E (u) = \int_{Ω} ∣ D u ∣^{2}$ (Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions, Orthogonality and the orthogonal complement). Then $S_{k}$ is nonempty, $E$ attains its infimum $μ_{k}$ on $S_{k}$ , every minimiser is a weak eigenpair with eigenvalue $μ_{k}$ , and $μ_{k} = λ_{k}$ (eigenvalues counted with multiplicity); moreover every minimiser lies in the eigenspace $E_{λ_{k}}$ and is orthogonal in $L^{2}$ to $e_{1}, \dots, e_{k - 1}$ .

Facts & Assumptions

Given: A nonempty bounded open set $Ω \subseteq R^{n}$ , the principal Dirichlet form $a_{0} (v, w) = \int_{Ω} D v \cdot D w$ with its eigenvalue list $λ_{1} \leq λ_{2} \leq \dots$ and orthonormal eigenbasis ${e_{j}}_{j \geq 1}$ of $L^{2} (Ω)$ , an index $k \geq 2$ , the set $S_{k}$ and the energy $E (v) = a_{0} (v, v)$ .

[F1]

Specialise the spectral theorem to the real form $a_{0} (v, w) = \int_{Ω} D v \cdot D w$ (identity principal coefficients, zero drift and potential). Discrete spectrum of a symmetric elliptic Dirichlet operator, Symmetric elliptic weak eigenpairs, The $L^{2}$ operator associated with a symmetric elliptic form: each $e_{j}$ lies in $H_{0}^{1} (Ω)$ with $∥ e_{j} ∥_{L^{2}} = 1$ , $a_{0} (e_{j}, v) = λ_{j} (e_{j}, v)_{L^{2}}$ for every $v \in H_{0}^{1} (Ω)$ , the list is nondecreasing, and ${e_{j}}$ is a Hilbert basis of $L^{2} (Ω)$ (Orthonormal families, complete orthonormal systems and Hilbert bases).

[F2]

Zero-boundary Sobolev space as a norm closure, $H^{k}$ is a Hilbert space under the derivative-sum inner product, A closed subspace of a Banach space is Banach: $H_{0}^{1} (Ω)$ is a closed subspace of $H^{1} (Ω) = W^{1, 2} (Ω)$ , hence a real Banach space, and under HB its closed subspace of the reflexive space $W^{1, 2} (Ω)$ is reflexive (W^{1,p}(Omega) is reflexive for 1<p<infinity, Closed subspaces of reflexive spaces are reflexive, Reflexivity is surjectivity of the canonical map).

[F3]

Convex and strictly convex functionals on a convex subset of a real vector space, A convex norm-lower-semicontinuous functional is weakly lower semicontinuous: $E$ is convex and continuous on $H_{0}^{1} (Ω)$ and therefore weakly sequentially lower semicontinuous on every nonempty convex subset (Axiom of Choice through the convex closedness lemma).

[F4]

A bounded sequence in a reflexive Banach space has a weakly convergent subsequence: under the ultrafilter lemma, DC and HB every norm-bounded sequence in a real reflexive Banach space has a weakly convergent subsequence.

[F5]

Weak H^1 convergence plus Rellich preserves the L^2 unit normalisation: for bounded open $Ω$ , if $(v_{j}) \subseteq H_{0}^{1} (Ω)$ is norm bounded with $v_{j} ⇀ v$ and $∥ v_{j} ∥_{L^{2}} = 1$ , then $∥ v ∥_{L^{2}} = 1$ .

[F6]

Smooth compactly supported functions of an open set are dense in $L^{2}$ , The space $L^{p} (μ)$ as the quotient by null functions: $H_{0}^{1} (Ω)$ is dense in $L^{2} (Ω)$ ; hence an $L^{2}$ class orthogonal to $H_{0}^{1} (Ω)$ is zero. For each $j$ the functional $L_{j} (v) : = (v, e_{j})_{L^{2}}$ is bounded on $H_{0}^{1} (Ω)$ because $∥ v ∥_{L^{2}} \leq ∥ v ∥_{H_{0}^{1}}$ , so $v_{j} ⇀ v$ in $H_{0}^{1} (Ω)$ implies $L_{j} (v_{j}) \to L_{j} (v)$ .

[F7]

The Lagrange multiplier rule for finitely many regular constraints, Fréchet derivative between Banach spaces: for a real Banach space $X$ , open $U \subseteq X$ , $I : U \to R$ Fréchet differentiable at $u$ and $G : U \to R^{m}$ of class $C^{1}$ with $D G (u)$ surjective, a local extremum of $I$ on the level set ${G = G (u)}$ admits a unique $λ \in R^{m}$ with $D I (u) = \sum_{i} λ_{i} D G_{i} (u)$ ; the Axiom of Choice is consumed here.

[F8]

Eigenfunctions for distinct symmetric elliptic eigenvalues are $L^{2}$ -orthogonal: weak eigenfunctions of the symmetric case with distinct eigenvalues are $L^{2}$ -orthogonal.

Proof

technique · direct

Given: The spectral data and the set $S_{k}$ above.

1.1givenF1

By [F1] the function $e_{k}$ has $∥ e_{k} ∥_{L^{2}} = 1$ and $(e_{k}, e_{j})_{L^{2}} = 0$ for $j < k$ , so $e_{k} \in S_{k}$ : the set $S_{k}$ is nonempty and $μ_{k} : = \inf_{S_{k}} E \leq E (e_{k}) = a_{0} (e_{k}, e_{k}) = λ_{k} ∥ e_{k} ∥_{L^{2}}^{2} = λ_{k} < \infty$ .

1.2F2F3F6

By [F2] the space $H_{0}^{1} (Ω)$ is a real reflexive Banach space, by [F3] the energy $E$ is weakly sequentially lower semicontinuous on $H_{0}^{1} (Ω)$ , and by [F6] each constraint functional $L_{j}$ , $j < k$ , is bounded on $H_{0}^{1} (Ω)$ .

2.1step 1.1step 1.2F4

Since $0 \leq μ_{k} < \infty$ , DC supplies a sequence $v_{j} \in S_{k}$ with $E (v_{j}) < μ_{k} + 1 / j$ for $j \geq 1$ , so $E (v_{j}) \to μ_{k}$ . Since $∥ v_{j} ∥_{L^{2}} = 1$ and $E (v_{j}) \leq λ_{k} + 1$ for all large $j$ , one has $∥ v_{j} ∥_{H_{0}^{1}}^{2} = 1 + E (v_{j}) \leq λ_{k} + 2$ ; by [F4] some subsequence satisfies $v_{j_{l}} ⇀ v_{0}$ in $H_{0}^{1} (Ω)$ .

3.1step 2.1F5F6

The limit stays constrained: [F5] applied to the subsequence gives $v_{0} \in H_{0}^{1} (Ω)$ and $∥ v_{0} ∥_{L^{2}} = 1$ , while for every $j < k$ the bounded functional $L_{j}$ of [F6] gives $(v_{0}, e_{j})_{L^{2}} = \lim_{l} (v_{j_{l}}, e_{j})_{L^{2}} = 0$ . Hence $v_{0} \in S_{k}$ .

4.1step 1.2step 2.1step 3.1F3

By weak lower semicontinuity [F3] we get $E (v_{0}) \leq {lim inf}_{l} E (v_{j_{l}}) = μ_{k}$ , and $v_{0} \in S_{k}$ gives $E (v_{0}) \geq μ_{k}$ ; hence $E (v_{0}) = μ_{k}$ , so $E$ attains its infimum on $S_{k}$ .

5.1step 4.1F1F6F7

Let $v_{0} \in S_{k}$ be any minimiser and define $G : X \to R^{k}$ on $X = H_{0}^{1} (Ω)$ by $G (u) = (∥ u ∥_{L^{2}}^{2} - 1, (u, e_{1})_{L^{2}}, \dots, (u, e_{k - 1})_{L^{2}})$ ; then ${G = 0} = S_{k} = {G = G (v_{0})}$ , $E$ and $G$ are Fréchet differentiable at $v_{0}$ with $D E (v_{0}) h = 2 \int_{Ω} D v_{0} \cdot D h$ and $D G (v_{0}) h = (2 (v_{0}, h)_{L^{2}}, (h, e_{1})_{L^{2}}, \dots, (h, e_{k - 1})_{L^{2}})$ , because the remainders are $\int_{Ω} ∣ D h ∣^{2}$ and the pairings $\int_{Ω} h^{2}$ . Surjectivity is explicit: $D G (v_{0}) (v_{0} / 2) = (1, 0, \dots, 0)$ and $D G (v_{0}) e_{j}$ is the standard coordinate vector with its $1$ in position $j + 1$ , for $j < k$ , using orthonormality and the constraints. The derivative formula holds at every $u \in X$ , its first component varies by at most $2 ∥ u - v ∥_{L^{2}} ∥ h ∥_{L^{2}} \leq 2 ∥ u - v ∥_{H^{1}} ∥ h ∥_{H^{1}}$ , and its other components are constant bounded functionals. Hence $G$ is $C^{1}$ with surjective derivative at $v_{0}$ , and [F7] gives unique multipliers $α, η_{1}, \dots, η_{k - 1} \in R$ with $2 a_{0} (v_{0}, h) = 2 α (v_{0}, h)_{L^{2}} + \sum_{j < k} η_{j} (h, e_{j})_{L^{2}}$ for every $h \in H_{0}^{1} (Ω)$ .

6.1step 4.1step 5.1F1

Test the identity of step 5.1 at $h = e_{j}$ with $j < k$ . Symmetry and [F1] give $2 a_{0} (v_{0}, e_{j}) = 2 λ_{j} (v_{0}, e_{j})_{L^{2}} = 0$ , whereas its right-hand side is $η_{j}$ by the constraints and orthonormality, so $η_{j} = 0$ . Testing at $h = v_{0}$ gives $2 E (v_{0}) = 2 α ∥ v_{0} ∥_{L^{2}}^{2}$ , so $α = μ_{k}$ . Therefore $a_{0} (v_{0}, h) = μ_{k} (v_{0}, h)_{L^{2}}$ for every $h \in H_{0}^{1} (Ω)$ , and every minimiser is a weak eigenpair with eigenvalue $μ_{k}$ .

7.1step 3.1step 6.1F1F8

It remains to identify $μ_{k}$ with $λ_{k}$ ; already $μ_{k} \leq λ_{k}$ by step 1.1. Suppose $μ_{k} < λ_{k}$ : for every $j \geq k$ one has $λ_{j} \geq λ_{k} > μ_{k}$ , so the eigenfunctions $v_{0}$ and $e_{j}$ have distinct eigenvalues and [F8] gives $(v_{0}, e_{j})_{L^{2}} = 0$ ; for $j < k$ the same holds because $v_{0} \in S_{k}$ . Thus $v_{0}$ is $L^{2}$ -orthogonal to every element of the Hilbert basis ${e_{j}}$ [F1], so $v_{0} = 0$ in $L^{2}$ , contradicting $∥ v_{0} ∥_{L^{2}} = 1$ . Hence $μ_{k} = λ_{k}$ .

8.1step 3.1step 4.1step 6.1step 7.1F1F2F4F3F7F8∎

Consequently $μ_{k} = λ_{k}$ , every minimiser is a weak eigenpair with eigenvalue $λ_{k}$ by step 6.1 and therefore lies in the eigenspace $E_{λ_{k}}$ , and by membership in $S_{k}$ it is $L^{2}$ -orthogonal to $e_{1}, \dots, e_{k - 1}$ . The Axiom of Choice enters through the convex-lower-semicontinuity and multiplier suppliers [F3, F7], Countable Choice through the orthogonality corollary [F8] (it follows from the assumed DC via Dependent choice implies countable choice), and the ultrafilter lemma, DC and HB through the weak-compactness and reflexivity suppliers [F2, F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

137 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

Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)
Richard S. Laugesen, Spectral Theory of Partial Differential Equations: Lecture Notes (arXiv:1203.2344, complete monograph) (standard reference, not scraped)