PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Smul

Real scaling of self-adjoint operators: self-adjointness and essential spectrum

Adapted from `adambornemann-glitch/Spectra`'s `SpectralTheory/Essential/Smul.lean` (Apache 2.0). Only the two lemmas that need no resolvent construction are ported here (**L1**, **L2** below); Spectra's third lemma, resolvent scaling (`selfAdjointResolvent (c•A − z)⁻¹ = c⁻¹•(A − z/c)⁻¹`), is **not** ported — this repo does not yet have a bounded-operator resolvent built directly from `IsSelfAdjoint` (see the docstring gap in `Weyl.lean`), and resolvent scaling itself is not needed for Weyl's theorem. See `EXTERNAL_INTEGRATION_PLAN.md` §3.4.

For an unbounded self-adjoint operator `A : H →ₗ.[ℂ] H` and a **real** nonzero scalar `c`:

* **L1** `isSelfAdjoint_smul_real` — `(c : ℂ) • A` is self-adjoint (formal self-adjointness for real `c` + surjectivity of `(c•A) ± i` via von Neumann's criterion, `IsSymmetric.isSelfAdjoint_of_range_eq_top`). * **L2** `essSpectrum_smul_real` — `essSpectrum (c • A) = (· * c) '' essSpectrum A` (Weyl sequences transfer: `(c•A − cλ)ψ = c•(A − λ)ψ`).

L1: self-adjointness under real scaling

L2: essential spectrum under real scaling

8 declarations

theorem

Real scalar multiples of formally self-adjoint operators are formally self-adjoint

#isFormalAdjoint_smul_real

Let $H$ be a complex Hilbert space and $A$ be a linear operator on $H$ . If $A$ is formally self-adjoint (i.e., symmetric on its domain), then for any real scalar $c \in \mathbb{R}$ , the scaled operator $c A$ is also formally self-adjoint.

theorem

Surjectivity of $A - zI$ for Self-Adjoint $A$ and $\operatorname{Im}(z) \neq 0$

#exists_apply_sub_smul_eq

Let $H$ be a Hilbert space and $A$ be a self-adjoint operator on $H$ . For any complex number $z$ with a non-zero imaginary part ( $\operatorname{Im}(z) \neq 0$ ) and any vector $\varphi \in H$ , there exists a vector $\psi$ in the domain of $A$ such that $A \psi - z \psi = \varphi$ .

theorem

$cA - w$ is Surjective for Real $c \neq 0$ and $\text{Im}(w) \neq 0$

#smul_surjective_sub_smul

Let $H$ be a complex Hilbert space and $A$ be a self-adjoint operator on $H$ . For any non-zero real number $c \in \mathbb{R}$ and any complex number $w \in \mathbb{C}$ such that its imaginary part is non-zero ( $\text{Im}(w) \neq 0$ ), the operator $c A - w I$ is surjective. That is, for every vector $\phi \in H$ , there exists a vector $\psi$ in the domain of the scaled operator $c A$ such that $(c A - w I) \psi = \phi$ .

theorem

Real scaling of a self-adjoint operator is self-adjoint

#isSelfAdjoint_smul_real

Let $H$ be a complex Hilbert space and $A$ be a self-adjoint operator on $H$ . For any non-zero real number $c \in \mathbb{R}$ , the scaled operator $cA$ is also self-adjoint.

theorem

$\lambda \in \sigma_{\text{ess}}(A) \implies c\lambda \in \sigma_{\text{ess}}(cA)$ for real $c \neq 0$

#mem_essSpectrum_smul_real

Let $H$ be a complex Hilbert space and $A$ be a self-adjoint operator on $H$ . For any non-zero real number $c \in \mathbb{R}$ , if a real number $\lambda$ is in the essential spectrum of $A$ (denoted $\sigma_{\text{ess}}(A)$ ), then the scaled value $c\lambda$ is in the essential spectrum of the scaled operator $cA$ . This is based on the fact that a Weyl sequence for $A$ at $\lambda$ can be transformed into a Weyl sequence for $cA$ at $c\lambda$ .

theorem

$A = B \implies \sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)$

#essSpectrum_congr_op

Let $H$ be a complex Hilbert space. Suppose $A$ and $B$ are self-adjoint linear operators on $H$ . If $A = B$ , then their essential spectra are equal: $\sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)$ . This confirms that the essential spectrum depends only on the operator itself and is independent of the specific proof (witness) of its self-adjointness.

theorem

$c^{-1} \cdot (c \cdot A) = A$ for real $c \neq 0$

#smul_inv_smul_pmap

Let $A$ be a partially defined linear operator on a complex Hilbert space $H$ . For any non-zero real number $c \in \mathbb{R}$ ( $c \neq 0$ ), scaling the operator $A$ by $c$ and then by its inverse $c^{-1}$ (where both are treated as complex scalars) is the identity operation on $A$ . That is, $c^{-1} \cdot (c \cdot A) = A$ .

theorem

Essential Spectrum of a Real Scaled Operator $\sigma_{\text{ess}}(cA) = c \cdot \sigma_{\text{ess}}(A)$

#essSpectrum_smul_real

Let $H$ be a complex Hilbert space and $A$ be a self-adjoint linear operator on $H$ . For any non-zero real number $c \in \mathbb{R}$ , the essential spectrum of the scaled operator $cA$ is the image of the essential spectrum of $A$ under multiplication by $c$ . That is, $\sigma_{\text{ess}}(cA) = \{ c\lambda \mid \lambda \in \sigma_{\text{ess}}(A) \}$ .

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Smul

Real scaling of self-adjoint operators: self-adjointness and essential spectrum

L1: self-adjointness under real scaling

L2: essential spectrum under real scaling

Real scalar multiples of formally self-adjoint operators are formally self-adjoint

Surjectivity of A−zIA - zIA−zI for Self-Adjoint AAA and Im⁡(z)≠0\operatorname{Im}(z) \neq 0Im(z)=0

cA−wcA - wcA−w is Surjective for Real c≠0c \neq 0c=0 and Im(w)≠0\text{Im}(w) \neq 0Im(w)=0

Real scaling of a self-adjoint operator is self-adjoint

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

A=B ⟹ σess(A)=σess(B)A = B \implies \sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)A=B⟹σess​(A)=σess​(B)

c−1⋅(c⋅A)=Ac^{-1} \cdot (c \cdot A) = Ac−1⋅(c⋅A)=A for real c≠0c \neq 0c=0

Essential Spectrum of a Real Scaled Operator σess(cA)=c⋅σess(A)\sigma_{\text{ess}}(cA) = c \cdot \sigma_{\text{ess}}(A)σess​(cA)=c⋅σess​(A)

Surjectivity of $A - zI$ for Self-Adjoint $A$ and $\operatorname{Im}(z) \neq 0$

$cA - w$ is Surjective for Real $c \neq 0$ and $\text{Im}(w) \neq 0$

$\lambda \in \sigma_{\text{ess}}(A) \implies c\lambda \in \sigma_{\text{ess}}(cA)$ for real $c \neq 0$

$A = B \implies \sigma_{\text{ess}}(A) = \sigma_{\text{ess}}(B)$

$c^{-1} \cdot (c \cdot A) = A$ for real $c \neq 0$

Essential Spectrum of a Real Scaled Operator $\sigma_{\text{ess}}(cA) = c \cdot \sigma_{\text{ess}}(A)$