PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Weyl

Weyl's theorem: invariance of the essential spectrum under a compact resolvent perturbation

Ported and adapted from `adambornemann-glitch/Spectra`'s `SpectralTheory/Essential/Weyl.lean` (Apache 2.0). See `EXTERNAL_INTEGRATION_PLAN.md` §3.4.

If `A`, `B` are self-adjoint operators whose resolvents at `i` differ by a **compact** operator, then `essSpectrum hA = essSpectrum hB`.

The missing bridge (honesty note)

Spectra proves this against its own `selfAdjointResolvent hA z hz : H →L[ℂ] H`, a genuine bounded operator built elsewhere in Spectra (`Spectra.Resolvent`) from `IsSelfAdjoint` alone: injectivity of `A − z•1` off the real axis (from symmetry) plus surjectivity (already available here, `LinearPMap.IsSelfAdjoint.sub_smul_surjective`) give a linear bijection `H ≃ A.domain`, and then a **closed graph theorem** argument upgrades continuity of the inverse to boundedness.

This repo already has the *partial-operator* resolvent `𝑅 T z := (T - z • 1).inverse` (`Physlib.QuantumMechanics.Operators.SpectralTheory.Basic`), and knows `𝑅 A z` is total (domain `⊤`) and continuous whenever `z ∈ resolventSet A` — but does not yet package "total + continuous" into a `H →L[ℂ] H` bundled continuous linear map (the last, purely bureaucratic step of the closed graph argument: `LinearMap.mkContinuous`-style repackaging of a `LinearPMap` with domain `⊤`). Building that packaging is a well-scoped, non-heroic remaining task (bounded by the 20–30 minute budget for this port, this file does not attempt it) — once it exists, `IsResolventAt` below becomes a *derived* fact about `𝑅 A I` rather than a standing hypothesis, and every theorem in this file specializes immediately (no proof surgery needed: only the hypothesis `hRA`/`hRB` needs discharging).

In the meantime, `IsResolventAt` axiomatizes exactly the three properties Spectra's `selfAdjointResolvent` is proved to have (`selfAdjointResolvent_mem_domain`, `selfAdjointResolvent_solves`, `selfAdjointResolvent_left_inverse`) and every theorem below is proved from those three properties alone — so the mathematical content of Weyl's theorem is fully ported and machine-checked; only the *existence* of a bounded resolvent operator satisfying them is left as a hypothesis instead of a constructed witness.

Main results

* `essSpectrum_subset_of_isCompactOperator_resolvent_sub` — one inclusion. * `essSpectrum_eq_of_isCompactOperator_resolvent_sub` — **Weyl's theorem**. * `essSpectrum_eq_of_isCompactOperator_perturb` — the relatively-compact-perturbation form (`B = A + (compact)·(resolvent)`), the form that applies to Schrödinger operators.

The bounded resolvent, axiomatized by its three defining properties

See the module docstring: this is the honesty-note bridge in place of a constructed bounded resolvent operator.

Weyl's theorem

On-ramp: relatively compact perturbations

5 declarations

theorem

$\text{Im}(i) \neq 0$

#I_im_ne_zero

The imaginary part of the imaginary unit $i$ is non-zero, i.e., $\text{Im}(i) \neq 0$ .

theorem

Essential Spectrum Inclusion under Compact Resolvent Perturbation

#essSpectrum_subset_of_isCompactOperator_resolvent_sub

Let $A$ and $B$ be self-adjoint operators on a complex Hilbert space $H$ . Let $R_A(i)$ and $R_B(i)$ be the bounded resolvent operators of $A$ and $B$ , respectively, evaluated at the imaginary unit $i$ . If the difference $R_B(i) - R_A(i)$ is a compact operator, then the essential spectrum of $A$ is a subset of the essential spectrum of $B$ : $\sigma_{\text{ess}}(A) \subseteq \sigma_{\text{ess}}(B)$

theorem

Weyl's Theorem: $\sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)$ for Compact Resolvent Perturbations

#essSpectrum_eq_of_isCompactOperator_resolvent_sub

Let $A$ and $B$ be self-adjoint operators on a complex Hilbert space $H$ . Let $R_A(i)$ and $R_B(i)$ be the bounded resolvent operators of $A$ and $B$ , respectively, at the imaginary unit $i \in \mathbb{C}$ . If the difference $R_B(i) - R_A(i)$ is a compact operator on $H$ , then the essential spectra of $A$ and $B$ are equal, denoted by $\sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)$ .

theorem

Relatively compact perturbation $B - A = W(A - iI)$ implies $R_B - R_A$ is compact

#isCompactOperator_resolvent_sub_of_isCompactOperator_perturb

Let $H$ be a complex Hilbert space. Let $A$ and $B$ be self-adjoint operators on $H$ with the same domain $D(A) = D(B)$ . Let $R_A$ and $R_B$ be the resolvent operators for $A$ and $B$ at $i$ (the imaginary unit), respectively. If there exists a compact operator $W: H \to H$ such that $(B - A)\chi = W(A - iI)\chi$ for all $\chi \in D(A)$ , then the difference of the resolvents $R_B - R_A$ is a compact operator.

theorem

Invariance of Essential Spectrum under Relatively Compact Perturbations (Weyl's Theorem)

#essSpectrum_eq_of_isCompactOperator_perturb

Let $H$ be a complex Hilbert space and let $A$ and $B$ be self-adjoint operators on $H$ with domains $D(A)$ and $D(B)$ , respectively. Suppose that $D(A) = D(B)$ . Let $R_A(i)$ and $R_B(i)$ be the bounded resolvent operators of $A$ and $B$ at the imaginary unit $i \in \mathbb{C}$ . If there exists a compact operator $W: H \to H$ such that for all $\psi \in D(A)$ , the relation $(B - A)\psi = W(A - iI)\psi$ holds (where $I$ is the identity operator), then the essential spectrum of $A$ is equal to the essential spectrum of $B$ : $\sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B).$

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Weyl

Weyl's theorem: invariance of the essential spectrum under a compact resolvent perturbation

The missing bridge (honesty note)

Main results

The bounded resolvent, axiomatized by its three defining properties

Weyl's theorem

On-ramp: relatively compact perturbations

Im(i)≠0\text{Im}(i) \neq 0Im(i)=0

Essential Spectrum Inclusion under Compact Resolvent Perturbation

Weyl's Theorem: σess(A)=σess(B)\sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)σess​(A)=σess​(B) for Compact Resolvent Perturbations

Relatively compact perturbation B−A=W(A−iI)B - A = W(A - iI)B−A=W(A−iI) implies RB−RAR_B - R_ARB​−RA​ is compact

Invariance of Essential Spectrum under Relatively Compact Perturbations (Weyl's Theorem)

$\text{Im}(i) \neq 0$

Weyl's Theorem: $\sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)$ for Compact Resolvent Perturbations

Relatively compact perturbation $B - A = W(A - iI)$ implies $R_B - R_A$ is compact