# Partially defined linear operators over topological vector spaces #

We define basic notions of partially defined linear operators, which we call unbounded operators for short. In this file we prove all elementary properties of unbounded operators that do not assume that the underlying spaces are normed.

## Main definitions #

`LinearPMap.IsClosed`

: An unbounded operator is closed iff its graph is closed.`LinearPMap.IsClosable`

: An unbounded operator is closable iff the closure of its graph is a graph.`LinearPMap.closure`

: For a closable unbounded operator`f : LinearPMap R E F`

the closure is the smallest closed extension of`f`

. If`f`

is not closable, then`f.closure`

is defined as`f`

.`LinearPMap.HasCore`

: a submodule contained in the domain is a core if restricting to the core does not lose information about the unbounded operator.

## Main statements #

`LinearPMap.closable_iff_exists_closed_extension`

: an unbounded operator is closable iff it has a closed extension.`LinearPMap.closable.exists_unique`

: there exists a unique closure`LinearPMap.closureHasCore`

: the domain of`f`

is a core of its closure

## References #

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

## Tags #

Unbounded operators, closed operators

### Closed and closable operators #

An unbounded operator is closed iff its graph is closed.

## Equations

## Instances For

An unbounded operator is closable iff the closure of its graph is a graph.

## Equations

- LinearPMap.IsClosable f = ∃ (f' : E →ₗ.[R] F), Submodule.topologicalClosure (LinearPMap.graph f) = LinearPMap.graph f'

## Instances For

A closed operator is trivially closable.

If `g`

has a closable extension `f`

, then `g`

itself is closable.

The closure is unique.

If `f`

is closable, then `f.closure`

is the closure. Otherwise it is defined
as `f.closure = f`

.

## Equations

- LinearPMap.closure f = if hf : LinearPMap.IsClosable f then Exists.choose hf else f

## Instances For

The closure (as a submodule) of the graph is equal to the graph of the closure
(as a `LinearPMap`

).

A `LinearPMap`

is contained in its closure.

If `f`

is closable, then the closure is closed.

If `f`

is closable, then the closure is closable.

### The core of a linear operator #

A submodule `S`

is a core of `f`

if the closure of the restriction of `f`

to `S`

is `f`

.

- le_domain : S ≤ f.domain
- closure_eq : LinearPMap.closure (LinearPMap.domRestrict f S) = f

## Instances For

For every unbounded operator `f`

the submodule `f.domain`

is a core of its closure.

Note that we don't require that `f`

is closable, due to the definition of the closure.

### Topological properties of the inverse #

If `f`

is invertible and closable as well as its closure being invertible, then
the graph of the inverse of the closure is given by the closure of the graph of the inverse.

Assuming that `f`

is invertible and closable, then the closure is invertible if and only
if the inverse of `f`

is closable.

If `f`

is invertible and closable, then taking the closure and the inverse commute.