PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Closed

The essential spectrum is closed

Ported, essentially verbatim, from `adambornemann-glitch/Spectra`'s `SpectralTheory/Essential/Closed.lean` (Apache 2.0).

`isClosed_essSpectrum` : for a self-adjoint operator `A`, `essSpectrum hA` is a closed subset of `ℝ`.

The proof is the standard diagonal argument. Given `λ_k ∈ essSpectrum` with `λ_k → λ`, each `λ_k` carries a singular sequence `(ψ_{k,n})_n`. All these vectors lie in a **separable** closed subspace `K` (the closed span of the countable family), which has a countable dense subset `{d_j}`. Choosing `n_k` so that `ψ_{k,n_k}` is simultaneously an approximate eigenvector of quality `1/(k+1)`, approximately normalized, and almost orthogonal to `d_0,…,d_k`, the diagonal sequence `φ_k := ψ_{k,n_k}` is a singular sequence for `λ` — weak nullness following from the orthogonal projection onto `K` together with the dense subset.

1 declaration

theorem

The essential spectrum $\sigma_{\mathrm{ess}}(A)$ is closed

#isClosed_essSpectrum

Let $H$ be a complex Hilbert space and $A$ be a self-adjoint linear operator on $H$ . The essential spectrum of $A$ , denoted by $\sigma_{\mathrm{ess}}(A)$ , is a closed subset of $\mathbb{R}$ .

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Closed

The essential spectrum is closed

The essential spectrum σess(A)\sigma_{\mathrm{ess}}(A)σess​(A) is closed

The essential spectrum $\sigma_{\mathrm{ess}}(A)$ is closed