Physicslib4.Spectral.Unbounded.Spectrum

The spectrum of an unbounded operator

For an unbounded operator T, a scalar λ lies in the resolvent set when T - λ 1 has a bounded two-sided inverse defined on all of H and landing in Dom(T); the spectrum is the complement. Since T - λ 1 is only defined on Dom(T), this is spelled out as a structure IsResolvent rather than as invertibility in a ring, so the names here are pmapResolventSet and pmapSpectrum to keep them apart from Mathlib's resolventSet and spectrum for bounded operators; pmapResolventSet_toPMap_top shows the two notions agree on bounded operators.

Main statements

• existsUnique_isResolvent — the inverse is unique when it exists.
• pmapResolventSet_toPMap_top, pmapSpectrum_toPMap_top — the two notions of spectrum agree for a bounded operator.
• sq_norm_le_of_isSymmetric — the b² inequality for a symmetric unbounded operator.
• pmapSpectrum_subset_real — the spectrum of an unbounded self-adjoint operator is real.
• isEssentiallySelfAdjoint_iff_dense_range — essential self-adjointness via dense range.

structure Physicslib4.Spectral.Unbounded.IsResolvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (lam : ℂ) (B : H →L[ℂ] H) : Prop

A bounded operator B is a two-sided inverse of T − λ𝟙: it maps H into Dom(T), and (T − λ𝟙)B = 𝟙 on H and B(T − λ𝟙) = 𝟙 on Dom(T).

For a bounded operator, λ is in the resolvent set when T − λ𝟙 has a bounded inverse. For an unbounded T the operator T − λ𝟙 is defined only on Dom(T), so "bounded inverse" has to be spelled out: B is defined and bounded on all of H, takes its values in Dom(T), and undoes T − λ𝟙 from both sides. Such a B is unique when it exists (existsUnique_isResolvent) and is written (T − λ𝟙)⁻¹. For a self-adjoint T and non-real λ it exists (mem_pmapResolventSet_of_im_ne_zero, whose proof bounds its norm by 1/|Im λ|).

Implementation note: the inverse is a predicate on a candidate B rather than an inverse in a ring, because Mathlib gives the partial maps H →ₗ.[ℂ] H no ring structure. The sign follows the blueprint, B = (T − λ𝟙)⁻¹; Mathlib's resolvent for bounded operators inverts λ𝟙 − A instead, the negative, which is why pmapResolventSet_toPMap_top passes through −B.

Blueprint: def:hall-9.16

• mem_domain (ψ : H) : B ψ ∈ T.domain

  B maps every vector of H into Dom(T).

• rightInverse (ψ : H) : ↑T ⟨B ψ, ⋯⟩ - lam • B ψ = ψ

  B is a right inverse: (T − λ𝟙)Bψ = ψ for every ψ in H.

• leftInverse (ψ : ↥T.domain) : B (↑T ψ - lam • ↑ψ) = ↑ψ

  B is a left inverse on the domain: B(T − λ𝟙)ψ = ψ for every ψ in Dom(T).

def Physicslib4.Spectral.Unbounded.pmapResolventSet {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) : Set ℂ

The resolvent set ρ(T) of an operator T: the complex numbers λ for which T − λ𝟙 has a bounded inverse defined on all of H.

A number λ is in ρ(T) when some bounded B satisfies IsResolvent T lam B. For a bounded operator on all of H this is the usual resolvent set (pmapResolventSet_toPMap_top). Its complement is the spectrum σ(T) (pmapSpectrum).

Implementation note: the prefix pmap (for LinearPMap) separates this from Mathlib's resolventSet for elements of an algebra.

Blueprint: def:hall-9.16

Equations

• Physicslib4.Spectral.Unbounded.pmapResolventSet T = {lam : ℂ | ∃ (B : H →L[ℂ] H), Physicslib4.Spectral.Unbounded.IsResolvent T lam B}

def Physicslib4.Spectral.Unbounded.pmapSpectrum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) : Set ℂ

The spectrum σ(T) of an operator T: the complex numbers λ for which T − λ𝟙 has no bounded inverse defined on all of H.

For a self-adjoint observable, σ(T) is the set of values a measurement can return. Besides eigenvalues it can contain continuous spectrum, such as all of ℝ for the momentum operator on L²(ℝ): there T − λ𝟙 is injective, but its inverse is not bounded and defined on all of H. The spectrum of a self-adjoint operator is real (pmapSpectrum_subset_real), and for a bounded operator on all of H it is the usual spectrum (pmapSpectrum_toPMap_top).

Implementation note: the complement of pmapResolventSet; the prefix pmap separates it from Mathlib's spectrum.

Blueprint: def:hall-9.16

Equations

• Physicslib4.Spectral.Unbounded.pmapSpectrum T = (Physicslib4.Spectral.Unbounded.pmapResolventSet T)ᶜ

theorem Physicslib4.Spectral.Unbounded.existsUnique_isResolvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} {lam : ℂ} (h : lam ∈ pmapResolventSet T) : ∃! B : H →L[ℂ] H, IsResolvent T lam B

The bounded inverse of T - λ 1 is unique when it exists; this is what licenses the notation (T - λ 1)⁻¹.

Blueprint reference: lmm:uniqueness-of-resolvent.

theorem Physicslib4.Spectral.Unbounded.pmapResolventSet_toPMap_top {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) : pmapResolventSet ((↑A).toPMap ⊤) = resolventSet ℂ A

For a bounded operator, regarded as an unbounded operator with domain all of H, the unbounded resolvent set agrees with Mathlib's resolventSet.

Blueprint reference: lmm:spectrum-notions-agree.

theorem Physicslib4.Spectral.Unbounded.pmapSpectrum_toPMap_top {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) : pmapSpectrum ((↑A).toPMap ⊤) = spectrum ℂ A

Consequently the two notions of spectrum agree for a bounded operator.

Blueprint reference: lmm:spectrum-notions-agree.

theorem Physicslib4.Spectral.Unbounded.sq_norm_le_of_isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hsym : IsSymmetric T) (a b : ℝ) (ψ : ↥T.domain) : b ^ 2 * ‖↑ψ‖ ^ 2 ≤ ‖↑T ψ - (↑a + ↑b * Complex.I) • ↑ψ‖ ^ 2

The b² inequality for a symmetric unbounded operator: for λ = a + i b with a, b real, b² ‖ψ‖² ≤ ‖(T - λ 1) ψ‖² for every ψ ∈ Dom(T).

This is the unbounded, merely-symmetric counterpart of lmm:hall-7.8 (Physicslib4.Spectral.sq_norm_sub_smul_apply_le).

Blueprint reference: lmm:b-squared-inequality-symmetric.

theorem Physicslib4.Spectral.Unbounded.abs_im_mul_norm_le_of_isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hsym : IsSymmetric T) (lam : ℂ) (ψ : ↥T.domain) : |lam.im| * ‖↑ψ‖ ≤ ‖↑T ψ - lam • ↑ψ‖

For a symmetric T, |Im λ| ‖ψ‖ ≤ ‖(T - λ 1) ψ‖ for every ψ ∈ Dom(T): the square root of the b² inequality sq_norm_le_of_isSymmetric.

Blueprint reference: thrm:hall-9.17.

theorem Physicslib4.Spectral.Unbounded.ker_subSmul_eq_bot {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hsym : IsSymmetric T) {lam : ℂ} (hlam : lam.im ≠ 0) : ker (subSmul T lam) = ⊥

For a symmetric T and non-real λ, the operator T - λ 1 is injective.

Blueprint reference: thrm:hall-9.17.

theorem Physicslib4.Spectral.Unbounded.range_subSmul_eq_top {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hsa : IsSelfAdjoint T) {lam : ℂ} (hlam : lam.im ≠ 0) : range (subSmul T lam) = ⊤

For a self-adjoint T and non-real λ, the operator T - λ 1 maps Dom(T) onto H.

Blueprint reference: thrm:hall-9.17.

theorem Physicslib4.Spectral.Unbounded.mem_pmapResolventSet_of_im_ne_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hsa : IsSelfAdjoint T) {lam : ℂ} (hlam : lam.im ≠ 0) : lam ∈ pmapResolventSet T

For a self-adjoint T, every non-real λ lies in the resolvent set of T: the inverse of the bijection T - λ 1 : Dom(T) → H is bounded by 1 / |Im λ|.

Blueprint reference: thrm:hall-9.17.

theorem Physicslib4.Spectral.Unbounded.pmapSpectrum_subset_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hsa : IsSelfAdjoint T) : pmapSpectrum T ⊆ {z : ℂ | z.im = 0}

The spectrum of a self-adjoint operator is contained in the real line.

This is why self-adjoint operators model observables: every possible measured value is real. For non-real λ = a + ib the estimate |b| ‖ψ‖ ≤ ‖(T − λ𝟙)ψ‖ on Dom(T), which needs only symmetry (abs_im_mul_norm_le_of_isSymmetric), makes T − λ𝟙 injective with closed range; its range is also dense, because its orthogonal complement is Ker(T* − λ̄𝟙) = Ker(T − λ̄𝟙) = {0}. So T − λ𝟙 maps Dom(T) onto H and its inverse is bounded by 1/|b|.

Implementation note: density of T.domain is not a separate hypothesis, since it follows from self-adjointness (Mathlib's IsSelfAdjoint.dense_domain). The real line is the set of z with z.im = 0.

Blueprint: thrm:hall-9.17

theorem Physicslib4.Spectral.Unbounded.dense_range_subSmul_of_isEssentiallySelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (h : IsEssentiallySelfAdjoint T) {lam : ℂ} (hlam : lam.im ≠ 0) : Dense ↑(range (subSmul T lam))

If T is essentially self-adjoint and λ is non-real, the range of T - λ 1 is dense.

Blueprint reference: thrm:hall-9.21 (forward direction).

theorem Physicslib4.Spectral.Unbounded.range_subSmul_eq_top_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T S : H →ₗ.[ℂ] H} (hS : S.IsClosed) (hsymS : IsSymmetric S) (hTS : T ≤ S) {lam : ℂ} (hlam : lam.im ≠ 0) (hd : Dense ↑(range (subSmul T lam))) : range (subSmul S lam) = ⊤

If S is a closed symmetric extension of T and λ is non-real, density of the range of T - λ 1 forces S - λ 1 to map Dom(S) onto H.

Blueprint reference: thrm:hall-9.21.

theorem Physicslib4.Spectral.Unbounded.adjoint_eq_of_range_eq_top {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : H →ₗ.[ℂ] H} (hle : S ≤ S.adjoint) {mu : ℂ} (hr : range (subSmul S mu) = ⊤) (hk : ker (subSmul S.adjoint mu) = ⊥) : S.adjoint = S

If S ≤ S*, S - μ 1 maps onto H and S* - μ 1 is injective, then S is self-adjoint.

Blueprint reference: thrm:hall-9.21.

theorem Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_iff_dense_range {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (hsym : IsSymmetric T) : IsEssentiallySelfAdjoint T ↔ Dense ↑(range (subSmul T Complex.I)) ∧ Dense ↑(range (subSmul T (-Complex.I)))

A densely defined symmetric operator T is essentially self-adjoint exactly when the ranges of T − i𝟙 and T + i𝟙 are both dense in H.

This is the working criterion for essential self-adjointness. To show that an operator written down on a convenient domain has a unique self-adjoint extension, it suffices to show that the equations (T ∓ i𝟙)ψ = φ can be solved for φ in a dense set of vectors. Equivalently, by Range(T ∓ i𝟙)ᗮ = Ker(T* ± i𝟙), the adjoint T* has no eigenvectors with eigenvalue ±i.

Implementation note: T + i𝟙 is subSmul T (-Complex.I).

Blueprint: thrm:hall-9.21