Unbounded operators

i. Overview

In this module we define unbounded operators between Hilbert spaces.

ii. Key results

Definitions:

• UnboundedOperator: Densely defined, closable unbounded operator between Hilbert spaces.
• partialOrder: Poset structure for unbounded operators.
• ofSymmetric: Construction of an unbounded operator from a symmetric LinearPMap.
• IsGeneralizedEigenvector: The notion of eigenvectors/values for linear functionals.

(In)equalities:

• le_closure: U ≤ U.closure
• adjoint_adjoint_eq_closure: U†† = U.closure
• adjoint_ge_adjoint_of_le: U₁ ≤ U₂ → U₂† ≤ U₁†
• closure_mono: U₁ ≤ U₂ → U₁.closure ≤ U₂.closure
• isSymmetric_iff_le_adjoint: IsSymmetric T ↔ T ≤ T†

iii. Table of contents

• A. Definition
• B. Basic identities
• C. Instances
  • C.1. Partial order
  • C.2. Zero
  • C.3. AddZeroClass
  • C.4. DistribSMul
• D. Closure
• E. Adjoint
• F. Symmetric operators
• G. Self-adjoint operators
• H. 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. Basic identities

theorem QuantumMechanics.UnboundedOperator.inner_map_polarization {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : UnboundedOperator H H} (x y : ↥T.domain) : inner ℂ (↑T.toLinearPMap x) ↑y = (inner ℂ (↑T.toLinearPMap (x + y)) ↑(x + y) - inner ℂ (↑T.toLinearPMap (x - y)) ↑(x - y) - Complex.I * inner ℂ (↑T.toLinearPMap (x + Complex.I • y)) ↑(x + Complex.I • y) + Complex.I * inner ℂ (↑T.toLinearPMap (x - Complex.I • y)) ↑(x - Complex.I • y)) / 4

theorem QuantumMechanics.UnboundedOperator.inner_map_polarization' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : UnboundedOperator H H} (x y : ↥T.domain) : inner ℂ (↑x) (↑T.toLinearPMap y) = (inner ℂ (↑(x + y)) (↑T.toLinearPMap (x + y)) - inner ℂ (↑(x - y)) (↑T.toLinearPMap (x - y)) - Complex.I * inner ℂ (↑(x + Complex.I • y)) (↑T.toLinearPMap (x + Complex.I • y)) + Complex.I * inner ℂ (↑(x - Complex.I • y)) (↑T.toLinearPMap (x - Complex.I • y))) / 4

C. Instances

C.1. 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.instPartialOrder {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.2. Zero

theorem QuantumMechanics.UnboundedOperator.isClosable_of_zero {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] {f : E →ₗ.[ℂ] F} (hf : ↑f = 0) : f.IsClosable

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

Equations

• QuantumMechanics.UnboundedOperator.instZero = { zero := { toLinearPMap := 0, dense_domain := ⋯, is_closable := ⋯ } }

@[simp]

theorem QuantumMechanics.UnboundedOperator.zero_toLinearPMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] : toLinearPMap 0 = 0

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

Equations

• QuantumMechanics.UnboundedOperator.instInhabited = { default := Zero.zero }

C.3. AddZeroClass

In defining addition for unbounded operators we use two junk values.

• If U₁.domain ∩ U₂.domain is not dense, then U₁ + U₂ = 0 (domain ⊤)
• If U₁.domain ∩ U₂.domain is dense but U₁.toLinearPMap + U₂.toLinearPMap is not closable, then U₁ + U₂ = 0 with domain U₁.domain ∩ U₂.domain. This ensures that distributivity, c • (U₁ + U₂) = c • U₁ + c • U₂, holds for (c : ℂ) = 0.

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

Equations

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

theorem QuantumMechanics.UnboundedOperator.add_domain_of_dense {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'} (hD : Dense (↑U₁.domain ⊓ ↑U₂.domain)) : (U₁ + U₂).domain = U₁.domain ⊓ U₂.domain

The domain of U₁ + U₂ is D(U₁) ∩ D(U₂) when it is dense.

theorem QuantumMechanics.UnboundedOperator.add_domain_of_not_dense {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'} (hD : ¬Dense (↑U₁.domain ⊓ ↑U₂.domain)) : (U₁ + U₂).domain = ⊤

The junk value for U₁ + U₂ has domain all of H when D(U₁) ∩ D(U₂) is not dense.

theorem QuantumMechanics.UnboundedOperator.mem_domain_of_dense {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'} (hD : Dense (↑U₁.domain ⊓ ↑U₂.domain)) (ψ : ↥(U₁ + U₂).domain) : ↑ψ ∈ U₁.domain ∧ ↑ψ ∈ U₂.domain

theorem QuantumMechanics.UnboundedOperator.add_toLinearPMap_of_dense_closable {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'} (hD : Dense (↑U₁.domain ⊓ ↑U₂.domain)) (hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) : (U₁ + U₂).toLinearPMap = U₁.toLinearPMap + U₂.toLinearPMap

U₁ + U₂ is the unbounded operator corresponding to U₁.toLinearPMap + U₂.toLinearPMap, provided it is both densely defined and closable.

theorem QuantumMechanics.UnboundedOperator.add_toLinearPMap_of_dense_not_closable {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'} (hD : Dense (↑U₁.domain ⊓ ↑U₂.domain)) (hC : ¬(U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) : (U₁ + U₂).toLinearPMap = { domain := U₁.domain ⊓ U₂.domain, toFun := 0 }

The junk value for U₁ + U₂ when D(U₁) ∩ D(U₂) is dense and U₁ + U₂ is not closable.

theorem QuantumMechanics.UnboundedOperator.add_toLinearPMap_of_not_dense {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'} (hD : ¬Dense (↑U₁.domain ⊓ ↑U₂.domain)) : (U₁ + U₂).toLinearPMap = 0

The junk value for U₁ + U₂ when D(U₁) ∩ D(U₂) is not dense.

theorem QuantumMechanics.UnboundedOperator.add_apply_of_dense_closable {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'} (hD : Dense (↑U₁.domain ⊓ ↑U₂.domain)) (hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) (ψ : ↥(U₁ + U₂).domain) : ↑(U₁ + U₂).toLinearPMap ψ = ↑U₁.toLinearPMap ⟨↑ψ, ⋯⟩ + ↑U₂.toLinearPMap ⟨↑ψ, ⋯⟩

(U₁ + U₂)ψ = U₁ψ + U₂ψ provided U₁ + U₂ is not given by a junk value.

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

Equations

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

theorem QuantumMechanics.UnboundedOperator.add_assoc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] {U₁ U₂ U₃ : UnboundedOperator H H'} (hD₁₂ : Dense (↑U₁.domain ⊓ ↑U₂.domain)) (hC₁₂ : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) (hD₂₃ : Dense (↑U₂.domain ⊓ ↑U₃.domain)) (hC₂₃ : (U₂.toLinearPMap + U₃.toLinearPMap).IsClosable) : U₁ + U₂ + U₃ = U₁ + (U₂ + U₃)

Addition of unbounded operators is associative when neither of the intermediate additions, U₁ + U₂ and U₂ + U₃, is given by a junk value.

C.4. DistribSMul

Scalar multiplication by complex numbers is inherited from LinearPMap. Note that (c : ℂ) • U has the same domain as U for all constants; in particular, (0 : ℂ) • U ≤ 0 with equality if and only if U.domain = ⊤.

theorem QuantumMechanics.UnboundedOperator.smul_mem_graph_of_mem_smul_graph {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] {f : E →ₗ.[ℂ] F} {c : ℂ} (hc : c ≠ 0) {x : E × F} (h : x ∈ (c • f).graph.topologicalClosure) : (x.1, c⁻¹ • x.2) ∈ f.graph.topologicalClosure

theorem QuantumMechanics.UnboundedOperator.smul_isClosable_of_isClosable {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] {f : E →ₗ.[ℂ] F} (hf : f.IsClosable) (c : ℂ) : (c • f).IsClosable

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

Equations

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

@[simp]

theorem QuantumMechanics.UnboundedOperator.smul_domain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H'] (U : UnboundedOperator H H') (c : ℂ) : (c • U).domain = U.domain

@[simp]

theorem QuantumMechanics.UnboundedOperator.smul_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') (c : ℂ) : (c • U).toLinearPMap = c • U.toLinearPMap

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

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

Equations

• QuantumMechanics.UnboundedOperator.instDistribSMulComplex = { toSMul := QuantumMechanics.UnboundedOperator.instSMulComplex, smul_zero := ⋯, smul_add := ⋯ }

D. 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

theorem QuantumMechanics.UnboundedOperator.isClosed_def {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.IsClosed ↔ U.closure = U

E. 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.adjoint_closure_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.adjoint.closure = U.adjoint

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

theorem QuantumMechanics.UnboundedOperator.isClosed_iff {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.IsClosed ↔ U.adjoint.adjoint = U

theorem QuantumMechanics.UnboundedOperator.adjoint_ge_adjoint_of_le {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₁ ≤ U₂) : U₂.adjoint ≤ U₁.adjoint

theorem QuantumMechanics.UnboundedOperator.closure_mono {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₁ ≤ U₂) : U₁.closure ≤ U₂.closure

F. 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 ψ)

def QuantumMechanics.UnboundedOperator.IsSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) : Prop

T is symmetric if ⟪T x, y⟫ = ⟪x, T y⟫ for all x,y ∈ T.domain.

Equations

• T.IsSymmetric = ∀ (x y : ↥T.domain), inner ℂ (↑T.toLinearPMap x) ↑y = inner ℂ (↑x) (↑T.toLinearPMap y)

theorem QuantumMechanics.UnboundedOperator.isSymmetric_iff_inner_map_self_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) : T.IsSymmetric ↔ ∀ (x : ↥T.domain), (starRingEnd ℂ) (inner ℂ (↑T.toLinearPMap x) ↑x) = inner ℂ (↑T.toLinearPMap x) ↑x

theorem QuantumMechanics.UnboundedOperator.isSymmetric_iff_le_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) : T.IsSymmetric ↔ T ≤ T.adjoint

G. 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

theorem QuantumMechanics.UnboundedOperator.isClosed_of_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : UnboundedOperator H H} (hT : IsSelfAdjoint T) : T.IsClosed

theorem QuantumMechanics.UnboundedOperator.isSymmetric_of_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : UnboundedOperator H H} (hT : IsSelfAdjoint T) : T.IsSymmetric

def QuantumMechanics.UnboundedOperator.IsEssentiallySelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : UnboundedOperator H H) : Prop

T is essentially self-adjoint if its closure is self-adjoint.

Equations

• T.IsEssentiallySelfAdjoint = IsSelfAdjoint T.closure

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

theorem QuantumMechanics.UnboundedOperator.isSelfAdjoint_isEssentiallySelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : UnboundedOperator H H} (hT : IsSelfAdjoint T) : T.IsEssentiallySelfAdjoint

H. 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(T) →L[ℂ] ℂ is a generalized eigenvector of an unbounded operator T if there is an eigenvalue c such that for all ψ ∈ D(T), F (T ψ) = 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 ψ