# mathlib3documentation

analysis.inner_product_space.linear_pmap

# Partially defined linear operators on Hilbert spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• linear_pmap.is_formal_adjoint: 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⟫.
• linear_pmap.adjoint: The adjoint of a map E →ₗ.[𝕜] F as a map F →ₗ.[𝕜] E.

## Main statements #

• linear_pmap.adjoint_is_formal_adjoint: The adjoint is a formal adjoint
• linear_pmap.is_formal_adjoint.le_adjoint: Every formal adjoint is contained in the adjoint
• continuous_linear_map.to_pmap_adjoint_eq_adjoint_to_pmap_of_dense: The adjoint on continuous_linear_map and linear_pmap coincide.

## Notation #

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

## Implementation notes #

We use the junk value pattern to define the adjoint for all linear_pmaps. 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 linear_pmap.is_formal_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ 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
@[protected]
theorem linear_pmap.is_formal_adjoint.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (h : T.is_formal_adjoint S) :
def linear_pmap.adjoint_domain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (T : E →ₗ.[𝕜] F) :
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.adjoint_domain.

Equations
def linear_pmap.adjoint_domain_mk_clm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (T : E →ₗ.[𝕜] F) (y : (T.adjoint_domain)) :
(T.domain) →L[𝕜] 𝕜

The operator λ x, ⟪y, T x⟫ considered as a continuous linear operator from T.adjoint_domain to 𝕜.

Equations
theorem linear_pmap.adjoint_domain_mk_clm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (T : E →ₗ.[𝕜] F) (y : (T.adjoint_domain)) (x : (T.domain)) :
x = (T x)
noncomputable def linear_pmap.adjoint_domain_mk_clm_extend {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : dense (T.domain)) (y : (T.adjoint_domain)) :
E →L[𝕜] 𝕜

The unique continuous extension of the operator adjoint_domain_mk_clm to E.

Equations
@[simp]
theorem linear_pmap.adjoint_domain_mk_clm_extend_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : dense (T.domain)) (y : (T.adjoint_domain)) (x : (T.domain)) :
= (T x)
noncomputable def linear_pmap.adjoint_aux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : dense (T.domain))  :

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

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

Equations
theorem linear_pmap.adjoint_aux_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : dense (T.domain)) (y : (T.adjoint_domain)) (x : (T.domain)) :
x = (T x)
theorem linear_pmap.adjoint_aux_unique {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : dense (T.domain)) (y : (T.adjoint_domain)) {x₀ : E} (hx₀ : (x : (T.domain)), x = (T x)) :
y = x₀
noncomputable def linear_pmap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (T : E →ₗ.[𝕜] F)  :
F →ₗ.[𝕜] E

The adjoint operator as a partially defined linear operator.

Equations
theorem linear_pmap.mem_adjoint_domain_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] (T : E →ₗ.[𝕜] F) (y : F) :
theorem linear_pmap.mem_adjoint_domain_of_exists {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (y : F) (h : (w : E), (x : (T.domain)), = (T x)) :
theorem linear_pmap.adjoint_apply_of_not_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : ¬dense (T.domain)) (y : (T.adjoint.domain)) :
theorem linear_pmap.adjoint_apply_of_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [ E] [ F] {T : E →ₗ.[𝕜] F} (hT : dense (T.domain)) (y : (T.adjoint.domain)) :
Restricting A to a dense submodule and taking the linear_pmap.adjoint is the same as taking the continuous_linear_map.adjoint interpreted as a linear_pmap.