Physlib

PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.Smul

Scaling self-adjoint operators

i. Overview

For a self-adjoint operator `A` and a real `c ≠ 0`, `c • A` is self-adjoint and its essential spectrum is the essential spectrum of `A` scaled by `c`.

ii. Key results

  • `isSelfAdjoint_smul_real` : `c • A` is self-adjoint.
  • `essSpectrum_smul_real` : the essential spectrum scales with `c`.

iii. Table of contents

  • A. L1: self-adjointness under real scaling
  • B. L2: essential spectrum under real scaling

iv. References

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

A. L1: self-adjointness under real scaling

B. L2: essential spectrum under real scaling

8 declarations

theorem

Real scaling preserves formal self-adjointness of operators

Let HH be a complex Hilbert space and AA be a formally self-adjoint linear operator on HH. For any real scalar c∈Rc \in \mathbb{R}, the scaled operator cAcA is also formally self-adjoint.

theorem

A−zIA - zI is Surjective for Self-Adjoint AA and z∉Rz \notin \mathbb{R}

Let AA be a self-adjoint operator on a complex Hilbert space HH. For any complex number z∈Cz \in \mathbb{C} off the real axis (i.e., Im⁡(z)≠0\operatorname{Im}(z) \neq 0), and for any vector ϕ∈H\phi \in H, there exists a vector ψ\psi in the domain of AA such that Aψ−zψ=ϕA\psi - z\psi = \phi.

theorem

Surjectivity of cA−wIcA - wI for self-adjoint AA and non-real ww

Let HH be a Hilbert space and AA be a self-adjoint linear operator on HH. For any non-zero real number c∈Rc \in \mathbb{R} and any complex number w∈Cw \in \mathbb{C} with a non-zero imaginary part (Im(w)≠0\text{Im}(w) \neq 0), the operator cA−wIcA - wI is surjective. Specifically, for every vector ϕ∈H\phi \in H, there exists a vector ψ\psi in the domain of the scaled operator cAcA such that (cA−wI)ψ=ϕ(cA - wI)\psi = \phi.

theorem

Real Scaling Preserves Self-Adjointness

Let AA be a self-adjoint operator on a complex Hilbert space HH. For any non-zero real number c∈Rc \in \mathbb{R}, the scaled operator cAc A is also self-adjoint.

theorem

λ∈σess(A)  ⟹  cλ∈σess(cA)\lambda \in \sigma_{\text{ess}}(A) \implies c\lambda \in \sigma_{\text{ess}}(cA) for real c≠0c \neq 0

Let HH be a complex Hilbert space and AA be a self-adjoint operator on HH. For any non-zero real number c∈Rc \in \mathbb{R}, if λ∈R\lambda \in \mathbb{R} is in the essential spectrum of AA, denoted σess(A)\sigma_{\text{ess}}(A), then cλc\lambda is in the essential spectrum of the scaled operator cAcA, denoted σess(cA)\sigma_{\text{ess}}(cA).

theorem

A=BA = B implies essSpectrum(A)=essSpectrum(B)\text{essSpectrum}(A) = \text{essSpectrum}(B)

Let HH be a complex Hilbert space. If AA and BB are self-adjoint linear operators on HH such that A=BA = B, then their essential spectra are equal: essSpectrum(A)=essSpectrum(B)\text{essSpectrum}(A) = \text{essSpectrum}(B). This theorem establishes that the essential spectrum is a property of the operator itself and is independent of the specific witness or proof used to demonstrate that the operator is self-adjoint.

theorem

c−1⋅(c⋅A)=Ac^{-1} \cdot (c \cdot A) = A for non-zero real cc

Let HH be a complex Hilbert space and AA be a linear operator on HH. For any non-zero real number c∈Rc \in \mathbb{R}, scaling AA by cc and then by its inverse c−1c^{-1} (where both are treated as complex scalars) returns the original operator AA. That is, c−1⋅(c⋅A)=Ac^{-1} \cdot (c \cdot A) = A.

theorem

essSpectrum(cA)=c⋅essSpectrum(A)\text{essSpectrum}(cA) = c \cdot \text{essSpectrum}(A) for c∈R∖{0}c \in \mathbb{R} \setminus \{0\}

Let HH be a complex Hilbert space and AA be a self-adjoint operator on HH. For any non-zero real number c∈Rc \in \mathbb{R}, the essential spectrum of the scaled operator cAc A is equal to the image of the essential spectrum of AA under scaling by cc. That is, essSpectrum(cA)={cμ∣μ∈essSpectrum(A)}\text{essSpectrum}(c A) = \{ c \mu \mid \mu \in \text{essSpectrum}(A) \}.