mathlib documentation


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 #

Main statements #

References #

Tags #

Unbounded operators, closed operators

Closed and closable operators #

def linear_pmap.is_closed {R : Type u_1} {E : Type u_2} {F : Type u_3} [comm_ring R] [add_comm_group E] [add_comm_group F] [module R E] [module R F] [topological_space E] [topological_space F] (f : E →ₗ.[R] F) :

An unbounded operator is closed iff its graph is closed.


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


A closed operator is trivially closable.

If g has a closable extension f, then g itself is closable.

If f is closable, then f.closure is the closure. Otherwise it is defined as f.closure = f.


The closure (as a submodule) of the graph is equal to the graph of the closure (as a linear_pmap).

A linear_pmap 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 again f.

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.