Physlib

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Defs

The essential spectrum (singular/Weyl-sequence definition)

Ported from `adambornemann-glitch/Spectra`'s `SpectralTheory/Essential/Defs.lean` (Apache 2.0), restated against this repo's own unbounded self-adjoint operator type `H →ₗ.[ℂ] H` / `LinearPMap.IsSelfAdjoint` (`Physlib.QuantumMechanics.Operators.SpectralTheory.SelfAdjoint`) instead of introducing a parallel one. See `EXTERNAL_INTEGRATION_PLAN.md` §3.4.

For a self-adjoint operator `A` (an unbounded `LinearPMap`) we define the **essential spectrum** `essSpectrum hA : Set ℝ` by *singular (Weyl) sequences*: `λ ∈ essSpectrum hA` iff there is a sequence `ψ : ℕ → A.domain` that is

* asymptotically normalized (`‖ψ n‖ → 1`), * weakly null (`⟪g, ψ n⟫ → 0` for every `g`), and * an approximate eigensequence (`‖A ψ n − λ ψ n‖ → 0`).

Weak nullness is exactly what is needed for the perturbation theorem (Weyl's theorem, see `Weyl.lean`): a relatively compact perturbation does not see a weakly-null approximate-eigenvector sequence. An *orthonormal* approximate eigensequence is a special case — orthonormal sequences are weakly null (`WeakCompact.lean`) — so this matches the classical Weyl-criterion definition.

  • `essSpectrum` : the essential spectrum of a self-adjoint `LinearPMap`.
  • `mem_essSpectrum_of_seq` : build membership from an `H`-valued Weyl sequence.
  • `essSpectrum_subset_spectrum` : the essential spectrum is contained in the spectrum.

2 declarations

definition

Essential spectrum σess(A)\sigma_{\text{ess}}(A) of a self-adjoint operator AA

Given a self-adjoint operator AA on a complex Hilbert space HH, the **essential spectrum** σess(A)\sigma_{\text{ess}}(A) is the set of real numbers λ∈R\lambda \in \mathbb{R} such that there exists a sequence (ψn)n∈N(\psi_n)_{n \in \mathbb{N}} in the domain of AA satisfying the following three conditions: 1. The sequence is asymptotically normalized: lim⁡n→∞∥ψn∥=1\lim_{n \to \infty} \|\psi_n\| = 1. 2. The sequence is weakly null: lim⁡n→∞⟨g,ψn⟩=0\lim_{n \to \infty} \langle g, \psi_n \rangle = 0 for every g∈Hg \in H. 3. The sequence is an approximate eigensequence for λ\lambda: lim⁡n→∞∥Aψn−λψn∥=0\lim_{n \to \infty} \|A \psi_n - \lambda \psi_n\| = 0.

theorem

Weyl's Criterion for Membership in the Essential Spectrum

Let HH be a complex Hilbert space and AA be a self-adjoint operator on HH with domain D(A)D(A). Let λ∈R\lambda \in \mathbb{R} and (ϕn)n∈N(\phi_n)_{n \in \mathbb{N}} be a sequence of vectors in HH. If the following conditions hold: 1. ϕn∈D(A)\phi_n \in D(A) for all n∈Nn \in \mathbb{N}; 2. The sequence is asymptotically normalized: lim⁡n→∞∥ϕn∥=1\lim_{n \to \infty} \|\phi_n\| = 1; 3. The sequence is weakly null: lim⁡n→∞⟨g,ϕn⟩=0\lim_{n \to \infty} \langle g, \phi_n \rangle = 0 for every g∈Hg \in H; 4. The sequence is an approximate eigensequence for λ\lambda: lim⁡n→∞∥Aϕn−λϕn∥=0\lim_{n \to \infty} \|A \phi_n - \lambda \phi_n\| = 0; then λ\lambda belongs to the essential spectrum σess(A)\sigma_{\text{ess}}(A).