# Documentation

Mathlib.Analysis.InnerProductSpace.LinearPMap

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

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

## Tags #

Unbounded operators, closed operators