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

## Tags #

Unbounded operators, closed operators

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

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 : { x : E // x T.domain }) (y : { x : F // x S.domain }), inner (T x) y = inner (↑x) (S y)
Instances For
theorem LinearPMap.IsFormalAdjoint.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (h : T.IsFormalAdjoint S) :
def LinearPMap.adjointDomain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (T : E →ₗ.[𝕜] 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' := }
Instances For
def LinearPMap.adjointDomainMkCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (T : E →ₗ.[𝕜] F) (y : { x : F // x T.adjointDomain }) :
{ x : E // x 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 := }
Instances For
theorem LinearPMap.adjointDomainMkCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (T : E →ₗ.[𝕜] F) (y : { x : F // x T.adjointDomain }) (x : { x : E // 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} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) (y : { x : F // x T.adjointDomain }) :
E →L[𝕜] 𝕜

The unique continuous extension of the operator adjointDomainMkCLM to E.

Equations
Instances For
@[simp]
theorem LinearPMap.adjointDomainMkCLMExtend_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) (y : { x : F // x T.adjointDomain }) (x : { x : E // x T.domain }) :
x = inner (↑y) (T x)
def LinearPMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [] :
{ x : F // x 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
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearPMap.adjointAux_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [] (y : { x : F // x T.adjointDomain }) (x : { x : E // x T.domain }) :
inner ( y) x = inner (↑y) (T x)
theorem LinearPMap.adjointAux_unique {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [] (y : { x : F // x T.adjointDomain }) {x₀ : E} (hx₀ : ∀ (x : { x : E // x T.domain }), inner x₀ x = inner (↑y) (T x)) :
y = x₀
def LinearPMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (T : E →ₗ.[𝕜] F) [] :
F →ₗ.[𝕜] E

The adjoint operator as a partially defined linear operator.

Equations
• T.adjoint = { domain := T.adjointDomain, toFun := if hT : Dense T.domain then else 0 }
Instances For
Equations
Instances For
theorem LinearPMap.mem_adjoint_domain_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] (T : E →ₗ.[𝕜] F) [] (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} [] [] [] {T : E →ₗ.[𝕜] F} [] (y : F) (h : ∃ (w : E), ∀ (x : { x : E // x T.domain }), inner w x = inner y (T x)) :
theorem LinearPMap.adjoint_apply_of_not_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} [] (hT : ¬Dense T.domain) (y : { x : F // x T.adjoint.domain }) :
theorem LinearPMap.adjoint_apply_of_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [] (y : { x : F // x T.adjoint.domain }) :
theorem LinearPMap.adjoint_apply_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [] (y : { x : F // x T.adjoint.domain }) {x₀ : E} (hx₀ : ∀ (x : { x : E // x T.domain }), inner x₀ x = inner (↑y) (T x)) :
theorem LinearPMap.adjoint_isFormalAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [] :

The fundamental property of the adjoint.

theorem LinearPMap.IsFormalAdjoint.le_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (hT : Dense T.domain) [] (h : T.IsFormalAdjoint S) :

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} [] [] [] [] [] (A : E →L[𝕜] F) {p : } (hp : Dense p) :

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} [] [] [] :
Star (E →ₗ.[𝕜] E)
Equations
• LinearPMap.instStar = { star := fun (A : E →ₗ.[𝕜] E) => A.adjoint }
theorem LinearPMap.isSelfAdjoint_def {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →ₗ.[𝕜] E} :
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.