Physlib

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.RealAnalytic

Reusable real-analytic certificates for unbounded observables

Contains only the represented operator facts needed to identify a self-adjoint (or essentially self-adjoint) `LinearPMap`: density, symmetry, defect indices, and the canonical closed extension. Keeping these certificates separate lets multiplication, Schrödinger, and oscillator models share the same analytic pipeline.

Main definitions

- `DefectIndexCertificate` / `DefectIndexCertificate.essentiallySelfAdjoint` : the von Neumann defect-index criterion for essential self-adjointness. - `isEssentiallySelfAdjoint_of_hilbertBasis_eigenvectors` : a symmetric operator whose domain is exactly the span of a Hilbert basis of eigenvectors with real eigenvalues is essentially self-adjoint (the "eigenbasis density" criterion).

Von Neumann's defect criterion

Essential self-adjointness from a Hilbert basis of eigenvectors

A symmetric operator whose domain is *exactly* the (algebraic) span of a Hilbert basis of eigenvectors with real eigenvalues is essentially self-adjoint. This is the standard "eigenbasis density" criterion for essential self-adjointness (see e.g. Reed–Simon, *Methods of Modern Mathematical Physics I: Functional Analysis*, Theorem VIII.3): reality of the eigenvalues makes `T ∓ i` bounded below by `1` on the eigenbasis span, and the Hilbert-basis expansion of an arbitrary `y : H` (with coefficients divided by `λ - z`) produces, in the limit of its partial sums, an explicit preimage of `y` under `T.closure ∓ i`.

4 declarations

theorem

A `DefectIndexCertificate` implies TT is essentially self-adjoint

Let HH be a complex Hilbert space and T:D(T)⊆H→HT: D(T) \subseteq H \to H be a partially defined linear operator. If TT possesses a `DefectIndexCertificate` (which verifies that TT is densely defined, symmetric, and has defect indices (0,0)(0,0) according to von Neumann's criterion), then TT is essentially self-adjoint.

theorem

A `DefectIndexCertificate` for TT implies Tˉ\bar{T} is self-adjoint

Let HH be a complex Hilbert space and T:D(T)⊆H→HT: D(T) \subseteq H \to H be a densely defined linear operator (represented as a `LinearPMap`). If TT has a `DefectIndexCertificate` (a certificate satisfying von Neumann's criterion, typically implying TT is symmetric and its defect indices are (0,0)(0, 0)), then the closure of TT, denoted Tˉ\bar{T}, is a self-adjoint operator.

theorem

T=T∗  ⟹  TT = T^* \implies T is essentially self-adjoint

Let HH be a complex Hilbert space. If a partially defined linear operator T:D(T)⊆H→HT: D(T) \subseteq H \to H is self-adjoint (meaning T=T∗T = T^*), then it is also essentially self-adjoint (meaning its closure T‾\overline{T} is self-adjoint).

theorem

An operator with a real-eigenvalue Hilbert basis span as its domain is essentially self-adjoint

Let HH be a complex Hilbert space and let {ei}i∈ι\{e_i\}_{i \in \iota} be a Hilbert basis for HH. Let TT be a partially defined linear operator on HH whose domain D(T)D(T) is exactly the algebraic span of the basis elements, D(T)=spanC{ei:i∈ι}D(T) = \text{span}_{\mathbb{C}} \{e_i : i \in \iota\}. If for each i∈ιi \in \iota, eie_i is an eigenvector of TT with a real eigenvalue λi∈R\lambda_i \in \mathbb{R} (such that Tei=λieiT e_i = \lambda_i e_i), then TT is essentially self-adjoint.