Unbounded operators

i. Overview

In this module we define unbounded operators on a Hilbert space.

ii. Key results

• UnboundedOperator : Densely defined, closable unbounded operators on a Hilbert space.
• IsGeneralizedEigenvector : The notion of eigenvector/value for linear functionals.

iii. Table of contents

• A. Definition
• B. Partial order
• C. Closure
• D. Adjoint
• E. Symmetric operators
• F. Self-adjoint operators
• G. Generalized eigenvectors

iv. References

• M. Reed & B. Simon, (1972). "Methods of modern mathematical physics: Vol. 1. Functional analysis". Academic Press. https://doi.org/10.1016/B978-0-12-585001-8.X5001-6
• K. Schmüdgen, (2012). "Unbounded self-adjoint operators on Hilbert space" (Vol. 265). Springer. https://doi.org/10.1007/978-94-007-4753-1

A. Definition

structure QuantumMechanics.UnboundedOperator (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (H' : Type u_2) [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] extends H →ₗ.[ℂ] H' : Type (max u_1 u_2)

An UnboundedOperator is a linear map from a submodule of H to H', assumed to be both densely defined and closable.

• domain : Submodule ℂ H
• toFun : ↥self.domain →ₗ[ℂ] H'
• dense_domain : Dense ↑self.domain

  The domain of an unbounded operator is dense in H.

• is_closable : self.IsClosable

  An unbounded operator is closable.

theorem QuantumMechanics.UnboundedOperator.ext {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] {U₁ U₂ : UnboundedOperator H H'} (h : U₁.toLinearPMap = U₂.toLinearPMap) : U₁ = U₂

theorem QuantumMechanics.UnboundedOperator.ext_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] {U₁ U₂ : UnboundedOperator H H'} : U₁ = U₂ ↔ U₁.toLinearPMap = U₂.toLinearPMap

instance QuantumMechanics.UnboundedOperator.instCoeFunForallSubtypeMemSubmoduleComplexDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] : CoeFun (UnboundedOperator H H') fun (U : UnboundedOperator H H') => ↥U.domain → H'

Equations

• QuantumMechanics.UnboundedOperator.instCoeFunForallSubtypeMemSubmoduleComplexDomain = { coe := fun (U : QuantumMechanics.UnboundedOperator H H') => ↑U.toLinearPMap }

B. Partial order

Unbounded operators inherit the structure of a poset from LinearPMap, but not that of a SemilatticeInf because U₁.domain ⊓ U₂.domain may not be dense.

instance QuantumMechanics.UnboundedOperator.partialOrder {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] : PartialOrder (UnboundedOperator H H')

Equations

• One or more equations did not get rendered due to their size.

C. Closure

noncomputable def QuantumMechanics.UnboundedOperator.closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : UnboundedOperator H H'

The closure of an unbounded operator.

Equations

• U.closure = { toLinearPMap := U.closure, dense_domain := ⋯, is_closable := ⋯ }

@[simp]

theorem QuantumMechanics.UnboundedOperator.closure_toLinearPMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U.closure.toLinearPMap = U.closure

theorem QuantumMechanics.UnboundedOperator.le_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U ≤ U.closure

def QuantumMechanics.UnboundedOperator.IsClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : Prop

An unbounded operator is closed iff the graph of its defining LinearPMap is closed.

Equations

• U.IsClosed = U.IsClosed

theorem QuantumMechanics.UnboundedOperator.closure_isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U.closure.IsClosed

D. Adjoint

theorem QuantumMechanics.UnboundedOperator.adjoint_dense_of_isClosable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] {f : H →ₗ.[ℂ] H'} (h_dense : Dense ↑f.domain) (h_closable : f.IsClosable) : Dense ↑f.adjoint.domain

The adjoint of a densely defined, closable LinearPMap is densely defined.

noncomputable def QuantumMechanics.UnboundedOperator.adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : UnboundedOperator H' H

The adjoint of an unbounded operator, denoted as U†.

Equations

• U.adjoint = { toLinearPMap := U.adjoint, dense_domain := ⋯, is_closable := ⋯ }

def QuantumMechanics.UnboundedOperator.«term_†» : Lean.TrailingParserDescr

The adjoint of an unbounded operator, denoted as U†.

Equations

• QuantumMechanics.UnboundedOperator.«term_†» = Lean.ParserDescr.trailingNode `QuantumMechanics.UnboundedOperator.«term_†» 1024 1024 (Lean.ParserDescr.symbol "†")

@[simp]

theorem QuantumMechanics.UnboundedOperator.adjoint_toLinearPMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U.adjoint.toLinearPMap = U.adjoint

theorem QuantumMechanics.UnboundedOperator.adjoint_isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U.adjoint.IsClosed

theorem QuantumMechanics.UnboundedOperator.closure_adjoint_eq_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U.closure.adjoint = U.adjoint

theorem QuantumMechanics.UnboundedOperator.adjoint_adjoint_eq_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U.adjoint.adjoint = U.closure

theorem QuantumMechanics.UnboundedOperator.le_adjoint_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') : U ≤ U.adjoint.adjoint

E. Symmetric operators

def QuantumMechanics.UnboundedOperator.ofSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense ↑E) {f : ↥E →ₗ[ℂ] ↥E} (hf : f.IsSymmetric) : UnboundedOperator H H

An UnboundedOperator constructed from a symmetric linear map on a dense submodule E.

Equations

• QuantumMechanics.UnboundedOperator.ofSymmetric hE hf = { domain := E, toFun := E.subtype ∘ₗ f, dense_domain := hE, is_closable := ⋯ }

@[simp]

theorem QuantumMechanics.UnboundedOperator.ofSymmetric_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense ↑E) {f : ↥E →ₗ[ℂ] ↥E} (hf : f.IsSymmetric) (ψ : ↥E) : ↑(ofSymmetric hE hf).toLinearPMap ψ = E.subtype (f ψ)

F. Self-adjoint operators

noncomputable instance QuantumMechanics.UnboundedOperator.instStar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Star (UnboundedOperator H H)

Equations

• QuantumMechanics.UnboundedOperator.instStar = { star := QuantumMechanics.UnboundedOperator.adjoint }

theorem QuantumMechanics.UnboundedOperator.isSelfAdjoint_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) : IsSelfAdjoint T ↔ T.adjoint = T

theorem QuantumMechanics.UnboundedOperator.isSelfAdjoint_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) : IsSelfAdjoint T ↔ IsSelfAdjoint T.toLinearPMap

G. Generalized eigenvectors

def QuantumMechanics.UnboundedOperator.IsGeneralizedEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) (F : ↥T.domain →L[ℂ] ℂ) (c : ℂ) : Prop

A map F : D(U) →L[ℂ] ℂ is a generalized eigenvector of an unbounded operator U if there is an eigenvalue c such that for all ψ ∈ D(U), F (U ψ) = c ⬝ F ψ.

Equations

• T.IsGeneralizedEigenvector F c = ∀ (ψ : ↥T.domain), ∃ (ψ' : ↥T.domain), ↑ψ' = ↑T.toLinearPMap ψ ∧ F ψ' = c • F ψ

theorem QuantumMechanics.UnboundedOperator.isGeneralizedEigenvector_ofSymmetric_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense ↑E) {f : ↥E →ₗ[ℂ] ↥E} (hf : f.IsSymmetric) (F : ↥E →L[ℂ] ℂ) (c : ℂ) : (ofSymmetric hE hf).IsGeneralizedEigenvector F c ↔ ∀ (ψ : ↥E), F (f ψ) = c • F ψ