Physlib Documentation

Physlib.QuantumMechanics.DDimensions.Operators.Unbounded

Unbounded operators #

i. Overview #

In this module we introduce unbounded operators on inner product spaces. By "unbounded operator" we mean a partially-defined linear map (LinearPMap) which is both densely defined and closable. These provide the mathematical structure appropriate for describing operators in non-relativistic quantum mechanics. Of particular interest are (essentially) self-adjoint unbounded operators since these correspond to physical observables.

Notes #

Naming convention : Definitions of LinearPMaps for quantum mechanical unbounded operators should have a name of the form […]Operator and notation should use calligraphic capital letters, e.g. mulOperator f (𝓜 f) for the multiplication operator associated with the function f.
Implementation : Although operators encountered in quantum mechanics are almost always unbounded, we opt to implement unbounded operators via the property IsUnbounded on LinearPMap rather than as a structure UnboundedOperator extending LinearPMap. The basic reason for this is that addition/subtraction and composition of unbounded operators in general does not result in another unbounded operator. This means, for example, that any attempt to define addition of UnboundedOperators would inevitably require introducing junk values that spoil associativity.

ii. Key results #

adjoint_add_le_add_adjoint : The inequality U₁† + U₂† ≤ (U₁ + U₂)† when U₁ + U₂ has dense domain.
IsEssentiallySelfAdjoint.unique_self_adjoint_extension : The closure of an essentially self-adjoint unbounded operator is its unique self-adjoint extension.
IsUnbounded.adjoint : The adjoint of an unbounded operator is also unbounded.
IsUnbounded.adjoint_closure_eq_adjoint : An unbounded operator and its closure have the same adjoint.
IsUnbounded.adjoint_adjoint_eq_closure : An unbounded operator U satisfies U†† = U.closure.

iii. Table of contents #

A. Definitions
B. Dense domain
C. Closability
D. Adjoints
E. Symmetric operators
F. Self-adjoint operators
G. Essentially self-adjoint operators
H. Unbounded operators

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. Definitions #

See LinearPMap.instStar and LinearPMap.isSelfAdjoint_def for the definition of IsSelfAdjoint for LinearPMaps.

def LinearPMap.HasDenseDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] (U : H →ₗ.[ℂ ] H') :

A LinearPMap U has dense domain iff U.domain is dense in H.

Equations

U.HasDenseDomain = Dense ↑U.domain

Instances For

theorem LinearPMap.hasDenseDomain_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} :

U.HasDenseDomain ↔ Dense ↑U.domain

def LinearPMap.IsUnbounded {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] (U : H →ₗ.[ℂ ] H') :

A LinearPMap is an unbounded operator iff it has dense domain and is closable.

Equations

U.IsUnbounded = (U.HasDenseDomain ∧ U.IsClosable)

Instances For

theorem LinearPMap.isUnbounded_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} :

U.IsUnbounded ↔ U.HasDenseDomain ∧ U.IsClosable

def LinearPMap.IsSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ ] H) :

A LinearPMap U is symmetric iff ⟪U x, y⟫_ℂ = ⟪x, U y⟫_ℂ for all x y : U.domain.

Equations

T.IsSymmetric = T.IsFormalAdjoint T

Instances For

theorem LinearPMap.isSymmetric_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} :

T.IsSymmetric ↔ T.IsFormalAdjoint T

def LinearPMap.IsEssentiallySelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →ₗ.[ℂ ] H) :

A LinearPMap is essentially self-adjoint iff its closure is self-adjoint.

Equations

T.IsEssentiallySelfAdjoint = IsSelfAdjoint T.closure

Instances For

theorem LinearPMap.isEssentiallySelfAdjoint_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] :

T.IsEssentiallySelfAdjoint ↔ IsSelfAdjoint T.closure

B. Dense domain #

theorem LinearPMap.HasDenseDomain.isUnbounded_iff_isClosable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.HasDenseDomain) :

U.IsUnbounded ↔ U.IsClosable

theorem LinearPMap.HasDenseDomain.closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.HasDenseDomain) :

U.closure.HasDenseDomain

theorem LinearPMap.HasDenseDomain.neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.HasDenseDomain) :

(-U).HasDenseDomain

theorem LinearPMap.HasDenseDomain.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.HasDenseDomain) (c : ℂ) :

(c • U).HasDenseDomain

theorem LinearPMap.HasDenseDomain.add_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U₁ U₂ : H →ₗ.[ℂ ] H'} (h₁ : U₁.HasDenseDomain) (h_le : U₁.domain ≤ U₂.domain) :

(U₁ + U₂).HasDenseDomain

theorem LinearPMap.HasDenseDomain.sub_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U₁ U₂ : H →ₗ.[ℂ ] H'} (h₁ : U₁.HasDenseDomain) (h_le : U₁.domain ≤ U₂.domain) :

(U₁ - U₂).HasDenseDomain

C. Closability #

theorem LinearPMap.IsClosable.isClosed_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.IsClosable) :

U.IsClosed ↔ U.closure = U

theorem LinearPMap.isClosable_of_exists_dense_formalAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] [CompleteSpace H'] (h : U.HasDenseDomain) (h_fadj : ∃ (U' : H' →ₗ.[ℂ ] H), U'.HasDenseDomain ∧ U'.IsFormalAdjoint U) :

A LinearPMap with densely-defined formal adjoint is closable.

theorem LinearPMap.isClosable_of_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h_zero : ↑U = 0) :

A zero LinearPMap (any domain) is closable.

theorem LinearPMap.IsClosable.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.IsClosable) (c : ℂ) :

(c • U).IsClosable

theorem LinearPMap.IsClosable.smul_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} {c : ℂ} (hc : c ≠ 0) :

(c • U).IsClosable ↔ U.IsClosable

theorem LinearPMap.neg_eq_neg_one_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] (U : H →ₗ.[ℂ ] H') :

-U = -1 • U

theorem LinearPMap.IsClosable.neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.IsClosable) :

(-U).IsClosable

theorem LinearPMap.closure_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] (U : H →ₗ.[ℂ ] H') {c : ℂ} (hc : c ≠ 0) :

(c • U).closure = c • U.closure

D. Adjoints #

theorem LinearPMap.adjoint_of_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] (h_zero : ↑U = 0) :

The adjoint of a zero LinearPMap (any domain) is zero (domain ⊤).

@[simp]

theorem LinearPMap.adjoint_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H] (U : H →ₗ.[ℂ ] H') {c : ℂ} (hc : c ≠ 0) :

(c • U).adjoint = (starRingEnd ℂ) c • U.adjoint

@[simp]

theorem LinearPMap.adjoint_neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H] (U : H →ₗ.[ℂ ] H') :

(-U).adjoint = -U.adjoint

theorem LinearPMap.adjoint_antitone {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U₁ U₂ : H →ₗ.[ℂ ] H'} [CompleteSpace H] (h₁₂ : U₁.HasDenseDomain ∨ ¬U₂.HasDenseDomain) (h_le : U₁ ≤ U₂) :

U₂.adjoint ≤ U₁.adjoint

theorem LinearPMap.adjoint_add_le_add_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H] (U₁ U₂ : H →ₗ.[ℂ ] H') (h₁₂ : (U₁ + U₂).HasDenseDomain) :

U₁.adjoint + U₂.adjoint ≤ (U₁ + U₂).adjoint

E. Symmetric operators #

theorem LinearPMap.inner_map_polarization {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} (x y : ↥T.domain) :

inner ℂ (↑T y) ↑x = (inner ℂ (↑T (x + y)) ↑(x + y) - inner ℂ (↑T (x - y)) ↑(x - y) + Complex.I * inner ℂ (↑T (x + Complex.I • y)) ↑(x + Complex.I • y) - Complex.I * inner ℂ (↑T (x - Complex.I • y)) ↑(x - Complex.I • y)) / 4

The analogue of inner_map_polarization for LinearPMap.

theorem LinearPMap.inner_map_polarization' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} (x y : ↥T.domain) :

inner ℂ (↑T x) ↑y = (inner ℂ (↑T (x + y)) ↑(x + y) - inner ℂ (↑T (x - y)) ↑(x - y) - Complex.I * inner ℂ (↑T (x + Complex.I • y)) ↑(x + Complex.I • y) + Complex.I * inner ℂ (↑T (x - Complex.I • y)) ↑(x - Complex.I • y)) / 4

The analogue of inner_map_polarization' for LinearPMap.

theorem LinearPMap.isSymmetric_iff_inner_map_self_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} :

T.IsSymmetric ↔ ∀ (x : ↥T.domain), (starRingEnd ℂ) (inner ℂ (↑T x) ↑x) = inner ℂ (↑T x) ↑x

theorem LinearPMap.IsSymmetric.isClosable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsSymmetric) (h' : T.HasDenseDomain) :

theorem LinearPMap.IsSymmetric.isUnbounded_iff_hasDenseDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsSymmetric) :

T.IsUnbounded ↔ T.HasDenseDomain

theorem LinearPMap.isSymmetric_iff_le_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.HasDenseDomain) :

T.IsSymmetric ↔ T ≤ T.adjoint

theorem LinearPMap.IsSymmetric.isSelfAdjoint_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsSymmetric) (h' : T.HasDenseDomain) :

IsSelfAdjoint T ↔ T.adjoint.domain = T.domain

theorem LinearPMap.add_adjoint_isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.HasDenseDomain) :

(T + T.adjoint).IsSymmetric

theorem LinearPMap.IsSymmetric.neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} (h : T.IsSymmetric) :

(-T).IsSymmetric

theorem LinearPMap.IsSymmetric.add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T₁ T₂ : H →ₗ.[ℂ ] H} (h₁ : T₁.IsSymmetric) (h₂ : T₂.IsSymmetric) :

(T₁ + T₂).IsSymmetric

theorem LinearPMap.IsSymmetric.sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T₁ T₂ : H →ₗ.[ℂ ] H} (h₁ : T₁.IsSymmetric) (h₂ : T₂.IsSymmetric) :

(T₁ - T₂).IsSymmetric

theorem LinearPMap.IsSymmetric.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} (h : T.IsSymmetric) {c : ℂ} (hc : (starRingEnd ℂ) c = c) :

(c • T).IsSymmetric

theorem LinearPMap.IsSymmetric.smul_ofReal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} (h : T.IsSymmetric) (r : ℝ) :

(↑r • T).IsSymmetric

theorem LinearPMap.IsSymmetric.of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T₁ T₂ : H →ₗ.[ℂ ] H} (h₁ : T₁.IsSymmetric) (h_le : T₂ ≤ T₁) :

T₂.IsSymmetric

F. Self-adjoint operators #

theorem LinearPMap.IsSelfAdjoint.isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

theorem LinearPMap.IsSelfAdjoint.isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

theorem LinearPMap.IsSelfAdjoint.isClosable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

theorem LinearPMap.IsSelfAdjoint.isUnbounded {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

theorem LinearPMap.IsSelfAdjoint.isEssentiallySelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

T.IsEssentiallySelfAdjoint

theorem LinearPMap.IsSelfAdjoint.adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

IsSelfAdjoint T.adjoint

theorem LinearPMap.IsSelfAdjoint.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) {c : ℂ} (hc : c ≠ 0) (hc' : (starRingEnd ℂ) c = c) :

IsSelfAdjoint (c • T)

theorem LinearPMap.IsSelfAdjoint.smul_ofReal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) {r : ℝ} (hr : r ≠ 0) :

IsSelfAdjoint (↑r • T)

theorem LinearPMap.IsSelfAdjoint.neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : IsSelfAdjoint T) :

IsSelfAdjoint (-T)

G. Essentially self-adjoint operators #

theorem LinearPMap.IsEssentiallySelfAdjoint.isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) :

theorem LinearPMap.IsEssentiallySelfAdjoint.isClosable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) (h' : T.HasDenseDomain) :

theorem LinearPMap.IsEssentiallySelfAdjoint.isUnbounded {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) (h' : T.HasDenseDomain) :

theorem LinearPMap.IsEssentiallySelfAdjoint.unique_self_adjoint_extension {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) (h' : T.HasDenseDomain) {T₂ : H →ₗ.[ℂ ] H} (h_le : T ≤ T₂) (h₂ : IsSelfAdjoint T₂) :

T₂ = T.closure

The closure is the unique self-adjoint extension of an essentially self-adjoint operator.

theorem LinearPMap.IsEssentiallySelfAdjoint.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) {c : ℂ} (hc : c ≠ 0) (hc' : (starRingEnd ℂ) c = c) :

(c • T).IsEssentiallySelfAdjoint

theorem LinearPMap.IsEssentiallySelfAdjoint.smul_ofReal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) {r : ℝ} (hr : r ≠ 0) :

(↑r • T).IsEssentiallySelfAdjoint

theorem LinearPMap.IsEssentiallySelfAdjoint.neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ ] H} [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) :

(-T).IsEssentiallySelfAdjoint

H. Unbounded operators #

theorem LinearPMap.IsUnbounded.hasDenseDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.IsUnbounded) :

U.HasDenseDomain

theorem LinearPMap.IsUnbounded.isClosable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.IsUnbounded) :

theorem LinearPMap.IsUnbounded.adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) :

U.adjoint.IsUnbounded

theorem LinearPMap.IsUnbounded.closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} (h : U.IsUnbounded) :

U.closure.IsUnbounded

@[simp]

theorem LinearPMap.IsUnbounded.adjoint_closure_eq_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] (h : U.IsUnbounded) :

U.closure.adjoint = U.adjoint

@[simp]

theorem LinearPMap.IsUnbounded.adjoint_adjoint_eq_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) :

U.adjoint.adjoint = U.closure

theorem LinearPMap.IsUnbounded.le_adjoint_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) :

U ≤ U.adjoint.adjoint

theorem LinearPMap.IsUnbounded.isClosed_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {H' : Type u_2} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] {U : H →ₗ.[ℂ ] H'} [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) :

U.IsClosed ↔ U.adjoint.adjoint = U

theorem LinearPMap.isUnbounded_of_dense_of_isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense ↑E) {f : ↥E →ₗ[ℂ ] H} (h : ∀ (x y : ↥E), inner ℂ (f x) ↑y = inner ℂ (↑x) (f y)) :

{ domain := E, toFun := f }.IsUnbounded

A LinearPMap constructed from a symmetric LinearMap with dense domain is an unbounded operator.

theorem LinearPMap.isUnbounded_of_dense_of_isSymmetric' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense ↑E) {f : ↥E →ₗ[ℂ ] ↥E} (h : f.IsSymmetric) :

{ domain := E, toFun := E.subtype ∘ₗ f }.IsUnbounded

Variant of of_dense_of_isSymmetric for an endomorphism satisfying LinearMap.IsSymmetric.