Partially defined linear operators on Hilbert spaces

We will develop the basics of the theory of unbounded operators on Hilbert spaces.

Main definitions

• LinearPMap.IsFormalAdjoint: An operator T is a formal adjoint of S if for all x in the domain of T and y in the domain of S, we have that ⟪T x, y⟫ = ⟪x, S y⟫.
• LinearPMap.adjoint: The adjoint of a map E →ₗ.[𝕜] F as a map F →ₗ.[𝕜] E.

Main statements

• LinearPMap.adjoint_isFormalAdjoint: The adjoint is a formal adjoint
• LinearPMap.IsFormalAdjoint.le_adjoint: Every formal adjoint is contained in the adjoint
• ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense: The adjoint on ContinuousLinearMap and LinearPMap coincide.

Notation

• For T : E →ₗ.[𝕜] F the adjoint can be written as T†. This notation is localized in LinearPMap.

Implementation notes

We use the junk value pattern to define the adjoint for all LinearPMaps. In the case that T : E →ₗ.[𝕜] F is not densely defined the adjoint T† is the zero map from T.adjoint.domain to E.

References

• [J. Weidmann, Linear Operators in Hilbert Spaces][weidmann_linear]

Tags

Unbounded operators, closed operators

def LinearPMap.IsFormalAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) (S : F →ₗ.[𝕜] E) : Prop

An operator T is a formal adjoint of S if for all x in the domain of T and y in the domain of S, we have that ⟪T x, y⟫ = ⟪x, S y⟫.

Equations

• T.IsFormalAdjoint S = ∀ (x : ↥T.domain) (y : ↥S.domain), inner 𝕜 (↑T x) ↑y = inner 𝕜 (↑x) (↑S y)

theorem LinearPMap.IsFormalAdjoint.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (h : T.IsFormalAdjoint S) : S.IsFormalAdjoint T

def LinearPMap.adjointDomain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) : Submodule 𝕜 F

The domain of the adjoint operator.

This definition is needed to construct the adjoint operator and the preferred version to use is T.adjoint.domain instead of T.adjointDomain.

Equations

• T.adjointDomain = { carrier := {y : F | Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def LinearPMap.adjointDomainMkCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) (y : ↥T.adjointDomain) : ↥T.domain →L[𝕜] 𝕜

The operator fun x ↦ ⟪y, T x⟫ considered as a continuous linear operator from T.adjointDomain to 𝕜.

Equations

• T.adjointDomainMkCLM y = { toLinearMap := (innerₛₗ 𝕜) ↑y ∘ₗ T.toFun, cont := ⋯ }

theorem LinearPMap.adjointDomainMkCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) (y : ↥T.adjointDomain) (x : ↥T.domain) : (T.adjointDomainMkCLM y) x = inner 𝕜 (↑y) (↑T x)

def LinearPMap.adjointDomainMkCLMExtend {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) (y : ↥T.adjointDomain) : E →L[𝕜] 𝕜

The unique continuous extension of the operator adjointDomainMkCLM to E.

Equations

• LinearPMap.adjointDomainMkCLMExtend hT y = (T.adjointDomainMkCLM y).extend T.domain.subtypeL ⋯ ⋯

@[simp]

theorem LinearPMap.adjointDomainMkCLMExtend_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) (y : ↥T.adjointDomain) (x : ↥T.domain) : (adjointDomainMkCLMExtend hT y) ↑x = inner 𝕜 (↑y) (↑T x)

def LinearPMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) [CompleteSpace E] : ↥T.adjointDomain →ₗ[𝕜] E

The adjoint as a linear map from its domain to E.

This is an auxiliary definition needed to define the adjoint operator as a LinearPMap without the assumption that T.domain is dense.

Equations

• LinearPMap.adjointAux hT = { toFun := fun (y : ↥T.adjointDomain) => (InnerProductSpace.toDual 𝕜 E).symm (LinearPMap.adjointDomainMkCLMExtend hT y), map_add' := ⋯, map_smul' := ⋯ }

theorem LinearPMap.adjointAux_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) [CompleteSpace E] (y : ↥T.adjointDomain) (x : ↥T.domain) : inner 𝕜 ((adjointAux hT) y) ↑x = inner 𝕜 (↑y) (↑T x)

theorem LinearPMap.adjointAux_unique {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) [CompleteSpace E] (y : ↥T.adjointDomain) {x₀ : E} (hx₀ : ∀ (x : ↥T.domain), inner 𝕜 x₀ ↑x = inner 𝕜 (↑y) (↑T x)) : (adjointAux hT) y = x₀

def LinearPMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) [CompleteSpace E] : F →ₗ.[𝕜] E

The adjoint operator as a partially defined linear operator, denoted as T†.

Equations

• T.adjoint = { domain := T.adjointDomain, toFun := if hT : Dense ↑T.domain then LinearPMap.adjointAux hT else 0 }

def LinearPMap.«term_†» : Lean.TrailingParserDescr

The adjoint operator as a partially defined linear operator, denoted as T†.

Equations

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

theorem LinearPMap.mem_adjoint_domain_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) [CompleteSpace E] (y : F) : y ∈ T.adjoint.domain ↔ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)

theorem LinearPMap.mem_adjoint_domain_of_exists {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} [CompleteSpace E] (y : F) (h : ∃ (w : E), ∀ (x : ↥T.domain), inner 𝕜 w ↑x = inner 𝕜 y (↑T x)) : y ∈ T.adjoint.domain

theorem LinearPMap.adjoint_apply_of_not_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} [CompleteSpace E] (hT : ¬Dense ↑T.domain) (y : ↥T.adjoint.domain) : ↑T.adjoint y = 0

theorem LinearPMap.adjoint_apply_of_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) [CompleteSpace E] (y : ↥T.adjoint.domain) : ↑T.adjoint y = (adjointAux hT) y

theorem LinearPMap.adjoint_apply_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) [CompleteSpace E] (y : ↥T.adjoint.domain) {x₀ : E} (hx₀ : ∀ (x : ↥T.domain), inner 𝕜 x₀ ↑x = inner 𝕜 (↑y) (↑T x)) : ↑T.adjoint y = x₀

theorem LinearPMap.adjoint_isFormalAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) [CompleteSpace E] : T.adjoint.IsFormalAdjoint T

The fundamental property of the adjoint.

theorem LinearPMap.IsFormalAdjoint.le_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (hT : Dense ↑T.domain) [CompleteSpace E] (h : T.IsFormalAdjoint S) : S ≤ T.adjoint

The adjoint is maximal in the sense that it contains every formal adjoint.

theorem ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) {p : Submodule 𝕜 E} (hp : Dense ↑p) : ((↑A).toPMap p).adjoint = (↑(adjoint A)).toPMap ⊤

Restricting A to a dense submodule and taking the LinearPMap.adjoint is the same as taking the ContinuousLinearMap.adjoint interpreted as a LinearPMap.

instance LinearPMap.instStar {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Star (E →ₗ.[𝕜] E)

Equations

• LinearPMap.instStar = { star := fun (A : E →ₗ.[𝕜] E) => A.adjoint }

theorem LinearPMap.isSelfAdjoint_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} : IsSelfAdjoint A ↔ A.adjoint = A

theorem IsSelfAdjoint.dense_domain {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) : Dense ↑A.domain

Every self-adjoint LinearPMap has dense domain.

This is not true by definition since we define the adjoint without the assumption that the domain is dense, but the choice of the junk value implies that a LinearPMap cannot be self-adjoint if it does not have dense domain.