Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Weyl's theorem: invariance of the essential spectrum

Statement

Assume the Axiom of Choice. Let A,C be self-adjoint operators such that RA(z)−RC(z) is compact for one nonreal z (equivalently, for every z∈ρ(A)∩ρ(C)). Then σess(A)=σess(C). In particular a bounded self-adjoint compact perturbation preserves the essential spectrum, and if K is symmetric and A-compact, then σess(A+K)=σess(A) with D(A+K)=D(A).

Facts & Assumptions

[A1]

λ∈σess(S) exactly when S has an orthonormal singular Weyl sequence at λ (Weyl criterion for the essential spectrum, Discrete and essential spectrum of a self-adjoint operator).

[A2]

For z∈ρ(S) and λ∈R one has RS(z)+1λ−zI=−1λ−zRS(z)(S−λ) on D(S), equivalently RS(z)(S−λ)=−(λ−z)(RS(z)+1λ−zI) (Resolvent and spectrum of an unbounded operator).

[A3]

A compact operator maps weakly convergent sequences to norm convergent sequences, and RS(z) is bounded (Compact operator sends weakly convergent sequences to norm convergent sequences, Compact linear operator).

[A4]

For self-adjoint A,C and nonreal z,w, the bounded resolvent identity gives Dw=[I+(w−z)RA(z)]−1Dz[I−(w−z)RC(w)], where Dz:=RA(z)−RC(z) and the inverse first factor is I+(z−w)RA(w). Hence compactness of Dz transfers to Dw, and conversely by exchanging z,w (The resolvent star algebra is dense in C_0(R), Compositions with a compact operator are compact).

[A5]

An A-compact symmetric K has A-bound zero, so Kato-Rellich makes A+K self-adjoint on D(A); the second resolvent identity RA+K(z)−RA(z)=RA+K(z)KRA(z) holds for z in the common resolvent set (Relative compactness with respect to an operator, Kato-Rellich theorem, Second resolvent identity for a closed perturbation).

Proof

technique · direct

Given: Self-adjoint A,C with compact resolvent difference at a nonreal z.

1.1A1A2A3

Let λ∈σess(A) and let (xn) be the orthonormal Weyl sequence of [A1]. By [A2] and ∥(A−λ)xn∥→0 one has (RA(z)+1λ−z)xn→0; since RA(z)−RC(z) is compact and xn⇀0, [A3] gives (RC(z)+1λ−z)xn→0 as well.

1.2A4

Parameter independence is [A4].

2.1A1A2step 1.1

Then (C−λ)RC(z)xn=(z−λ)RC(z)xn−xn→0 by [A2] and step 1.1, and ∥RC(z)xn∥→∣λ−z∣−1>0; the normalized vectors yn:=∥RC(z)xn∥−1RC(z)xn lie in D(C), have unit norm, converge weakly to 0 and satisfy (C−λ)yn→0, so they form a singular Weyl sequence and λ∈σess(C) by [A1]. Interchanging the roles of A and C gives equality.

3.1A4A5step 2.1

Bounded compact perturbations: if K is bounded, symmetric and compact, then A+K is self-adjoint with D(A+K)=D(A) by Kato-Rellich applied with the admissible pair (0,∥K∥), and the second resolvent identity gives RA+K(z)−RA(z)=RA+K(z)KRA(z), compact as a product of the compact K with bounded factors; so σess(A+K)=σess(A) by step 2.1.

3.2A5step 2.1

A-compact perturbations: for symmetric K that is A-compact, [A5] makes A+K self-adjoint with D(A+K)=D(A) and gives RA+K(z)−RA(z)=RA+K(z)KRA(z), a product of the bounded operator RA+K(z) with the compact operator KRA(z), hence compact; then step 2.1 applies.

4.1

The claims are steps 1.1, 1.2 and 2.1 (compact resolvent difference), 3.1 (bounded compact perturbations) and 3.2 (A-compact perturbations). ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

73 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