PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.Closed

The essential spectrum is closed

i. Overview

The essential spectrum of a self-adjoint operator is closed. For `λₖ → λ` in the essential spectrum, all singular sequences of the `λₖ` lie in a separable closed subspace. A diagonal choice, almost orthogonal to more and more vectors of a countable dense subset, is a singular sequence for `λ`.

ii. Key results

`isClosed_essSpectrum` : the essential spectrum is closed.

iii. References

Adapted from `adambornemann-glitch/Spectra`, `SpectralTheory/Essential/Closed.lean` (Apache 2.0).

1 declaration

theorem

The essential spectrum of a self-adjoint operator is closed

#isClosed_essSpectrum

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