LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Spectral convergence under collectively compact positive approximations

Statement

Assume Countable Choice. Let $H$ be a real Hilbert space. Let $T : H \to H$ and $T_{n} : H \to H$ be compact, self-adjoint, nonnegative operators. Assume $T_{n} x \to T x$ in norm for every $x \in H$ , $\sup_{n} ∥ T_{n} ∥ < \infty$ , and the family is sequentially collectively compact: for every strictly increasing sequence $(n_{j})$ and every bounded sequence $(x_{j})$ , the sequence $(T_{n_{j}} x_{j})$ has a norm-convergent subsequence. Then:

For every strictly increasing sequence $(n_{j})_{j \geq 1}$ in $N$ , if $μ_{j} > 0$ is an eigenvalue of $T_{n_{j}}$ and $μ_{j} \to μ > 0$ , then $μ$ is an eigenvalue of $T$ . Thus no positive spectral limit is spurious.
If $μ > 0$ is an isolated eigenvalue of $T$ with multiplicity $m = \dim \ker (T - μ I)$ , then for all sufficiently large $n$ the open interval $I = (μ - δ, μ + δ)$ , chosen so that $μ - δ > 0$ and $\overline{I} \cap σ (T) = {μ}$ , contains exactly $m$ eigenvalues of $T_{n}$ , counted with multiplicity. Their distance to $μ$ tends to zero, and the associated eigenspaces converge to $\ker (T - μ I)$ in symmetric $H$ -gap.

Here $σ (T)$ denotes the spectrum, and the symmetric gap between finite-dimensional subspaces $E, F$ is $\max {\sup_{x \in E, ∥ x ∥ = 1} dist (x, F), \sup_{y \in F, ∥ y ∥ = 1} dist (y, E)} .$

Facts & Assumptions

Given: Countable Choice; a real Hilbert space $H$ ; compact nonnegative self-adjoint operators $T, T_{n}$ satisfying the strong-convergence, uniform operator-bound and sequential collective-compactness hypotheses.

[A1]

Countable Choice is assumed in the compact self-adjoint spectral theorem and selects the eigenvectors and cluster vectors used in the sequential contradictions below. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

A compact self-adjoint operator has finite-dimensional eigenspaces for nonzero eigenvalues, and its nonzero spectral subspace is the orthogonal sum of those eigenspaces; for every $ε > 0$ , only finitely many nonzero eigenvalues have absolute value at least $ε$ . (Spectral theorem for compact self adjoint operators)

[F2]

A linear map from an $m$ -dimensional space to a space of dimension less than $m$ has a nonzero kernel. (Rank-nullity: $\dim_{F} V = nullity T + rank T$ )

[F3]

A closed subspace of a Hilbert space has an orthogonal projection, and the distance to it is the norm of the orthogonal residual. (Orthogonal decomposition by a closed subspace)

[F4]

Every bounded real sequence has a convergent subsequence. (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence)

Proof

Given: The data in the statement, an isolated positive eigenvalue $μ$ of $T$ , and a closed interval $\overline{I} \subset (0, \infty)$ containing no point of $σ (T)$ other than $μ$ .

1.1A1givenchoosealgebra

Let $n_{1} < n_{2} < \dots$ and let $μ_{j} > 0$ be eigenvalues of $T_{n_{j}}$ converging to $ν > 0$ , and choose unit eigenvectors $x_{j}$ with $T_{n_{j}} x_{j} = μ_{j} x_{j}$ . Sequential collective compactness gives a subsequence for which $T_{n_{j}} x_{j} \to y$ . Since $μ_{j} \to ν > 0$ , $x_{j} \to x : = y / ν$ and $∥ x ∥ = 1$ . The uniform operator bound gives $∥ T_{n_{j}} (x_{j} - x) ∥ \leq (\sup_{n} ∥ T_{n} ∥) ∥ x_{j} - x ∥ \to 0$ ; strong convergence gives $T_{n_{j}} x \to T x$ . Hence $T x = y = ν x$ , so $ν$ is an eigenvalue of $T$ .

1.2F1givenchoose

By [F1], $E : = \ker (T - μ I)$ is finite-dimensional; write $m = \dim E$ . Choose $δ > 0$ so that $I = (μ - δ, μ + δ)$ has $μ - δ > 0$ and $\overline{I} \cap σ (T) = {μ}$ . Let $E_{n}$ be the orthogonal sum of the eigenspaces of $T_{n}$ whose eigenvalues lie in $I$ . This sum is finite-dimensional because [F1] permits only finitely many eigenvalues outside a neighborhood of zero, and $I$ stays away from zero.

2.1A1F1F2givenstep 1.2algebra

If $\dim E_{n} < m$ for infinitely many $n$ , the orthogonal projection $P_{n} : H \to E_{n}$ restricts to a linear map from $E$ to a space of dimension less than $m$ . By [F2] choose a unit $x_{n} \in E$ with $P_{n} x_{n} = 0$ . The compact self-adjoint spectral expansion of $T_{n}$ then gives $∥ (T_{n} - μ I) x_{n} ∥ \geq δ$ , since every spectral value in the orthogonal complement of $E_{n}$ is at distance at least $δ$ from $μ$ . Strong convergence is uniform on the finite-dimensional unit sphere of $E$ : for an orthonormal basis $e_{1}, \dots, e_{m}$ , write $x = \sum_{i} c_{i} e_{i}$ and bound $∥ (T_{n} - T) x ∥ \leq \sum_{i} ∣ c_{i} ∣ ∥ (T_{n} - T) e_{i} ∥$ . Since $T x_{n} = μ x_{n}$ , this uniform convergence contradicts the lower bound. Therefore $\dim E_{n} \geq m$ for all sufficiently large $n$ .

3.1A1F1F4step 1.1step 2.1algebra

If $\dim E_{n} \geq m + 1$ for infinitely many $n$ , select $m + 1$ orthonormal eigenvectors $x_{n, 1}, \dots, x_{n, m + 1}$ in $E_{n}$ . Apply [F4] successively to these finitely many eigenvalue sequences to obtain one subsequence on which all converge in $\overline{I}$ . By step 1.1 every such limit is in $σ (T)$ , hence equals $μ$ . Sequential collective compactness, applied successively to the finite list of sequences $T_{n} x_{n, i}$ , gives a subsequence on which all these images converge. Their eigenvalues stay bounded away from zero, so all $x_{n, i}$ converge in norm. Their limits remain orthonormal and, by step 1.1, lie in $E$ , contradicting $\dim E = m$ . Thus $\dim E_{n} \leq m$ for all sufficiently large $n$ , and together with step 2.1 the dimension equals $m$ .

4.1A1F4givenstep 1.1step 3.1algebra

The eigenvalues of $T_{n}$ in $I$ all converge to $μ$ : otherwise a subsequence stays a positive distance from $μ$ and has a convergent subsequence in $\overline{I}$ by [F4]; step 1.1 makes its limit a spectral point of $T$ , while $\overline{I} \cap σ (T) = {μ}$ . Let $E_{n}$ continue to denote the $m$ -dimensional cluster subspace. If unit vectors $x_{n} \in E_{n}$ had $dist (x_{n}, E) \geq ε > 0$ , the convergence just proved would give $∥ (T_{n} - μ I) x_{n} ∥ \to 0$ . Collective compactness yields a subsequence with $T_{n} x_{n}$ convergent; then $x_{n}$ converges to a unit $x$ and the argument of step 1.1 gives $T x = μ x$ , contradicting the distance bound. Thus $\sup_{x \in E_{n}, ∥ x ∥ = 1} dist (x, E) \to 0$ .

5.1F1F3givenstep 4.1algebra∎

For $x \in E$ , let $P_{n}$ be the orthogonal projection onto $E_{n}$ . On $E_{n}^{⊥}$ , the spectrum of $T_{n}$ stays at distance at least $δ$ from $μ$ . The spectral expansion therefore gives $∥ x - P_{n} x ∥ \leq δ^{- 1} ∥ (T_{n} - μ I) x ∥$ . Strong convergence of $T_{n}$ to $T$ is uniform on the finite-dimensional space $E$ , and $T x = μ x$ there, so the right side tends uniformly to zero for unit $x \in E$ . Hence $\sup_{x \in E, ∥ x ∥ = 1} dist (x, E_{n}) \to 0$ . Combined with the directed-gap limit proved in step 4.1, this is symmetric-gap convergence. The multiplicity and no-pollution conclusions follow.

Source notes

Boffi's complete course notes develop compact solution operators, absence of spurious modes, full multiplicity and eigenspace-gap convergence in the general Galerkin setting (slides 102–108). This carrier proves the self-adjoint positive operator version locally; the source does not replace that argument.

Depends on

Used by

Spectral convergence and no nonzero pollution for PEC edge elements Theorem

Dependency tree · two levels

64 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

Peter Monk, Finite Element Methods for Maxwell's Equations, Oxford University Press, 2003 (standard reference, not scraped)
Daniele Boffi, Finite element approximation of eigenvalue problems, complete Pavia course notes, 2017 (standard reference, not scraped)