Partially defined linear operators over topological vector spaces #

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

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 #

linear_pmap.is_closed: An unbounded operator is closed iff its graph is closed.
linear_pmap.is_closable: An unbounded operator is closable iff the closure of its graph is a graph.
linear_pmap.closure: For a closable unbounded operator f : linear_pmap R E F the closure is the smallest closed extension of f. If f is not closable, then f.closure is defined as f.
linear_pmap.has_core: a submodule contained in the domain is a core if restricting to the core does not lose information about the unbounded operator.

Main statements #

linear_pmap.closable_iff_exists_closed_extension: an unbounded operator is closable iff it has a closed extension.
linear_pmap.closable.exists_unique: there exists a unique closure
linear_pmap.closure_has_core: the domain of f is a core of its closure

References #

J. Weidmann, Linear Operators in Hilbert Spaces

Tags #

Unbounded operators, closed operators

Closed and closable operators #

source

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) :

Prop

An unbounded operator is closed iff its graph is closed.

Equations

f.is_closed = is_closed ↑(f.graph)

source

def linear_pmap.is_closable {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] (f : E →ₗ.[R] F) :

Prop

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

Equations

f.is_closable = ∃ (f' : E →ₗ.[R] F), f.graph.topological_closure = f'.graph

source

theorem linear_pmap.is_closed.is_closable {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : f.is_closed) :

f.is_closable

A closed operator is trivially closable.

source

theorem linear_pmap.is_closable.le_is_closable {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f g : E →ₗ.[R] F} (hf : f.is_closable) (hfg : g ≤ f) :

g.is_closable

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

source

theorem linear_pmap.is_closable.exists_unique {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : f.is_closable) :

∃! (f' : E →ₗ.[R] F), f.graph.topological_closure = f'.graph

The closure is unique.

source

noncomputable def linear_pmap.closure {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] (f : E →ₗ.[R] F) :

E →ₗ.[R] F

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

Equations

f.closure = dite f.is_closable (λ (hf : f.is_closable), Exists.some hf) (λ (hf : ¬f.is_closable), f)

source

theorem linear_pmap.closure_def {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : f.is_closable) :

f.closure = Exists.some hf

source

theorem linear_pmap.closure_def' {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : ¬f.is_closable) :

f.closure = f

source

theorem linear_pmap.is_closable.graph_closure_eq_closure_graph {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : f.is_closable) :

f.graph.topological_closure = f.closure.graph

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

source

theorem linear_pmap.le_closure {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] (f : E →ₗ.[R] F) :

f ≤ f.closure

A linear_pmap is contained in its closure.

source

theorem linear_pmap.is_closable.closure_mono {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f g : E →ₗ.[R] F} (hg : g.is_closable) (h : f ≤ g) :

f.closure ≤ g.closure

source

theorem linear_pmap.is_closable.closure_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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : f.is_closable) :

f.closure.is_closed

If f is closable, then the closure is closed.

source

theorem linear_pmap.is_closable.closure_is_closable {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} (hf : f.is_closable) :

f.closure.is_closable

If f is closable, then the closure is closable.

source

theorem linear_pmap.is_closable_iff_exists_closed_extension {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} :

f.is_closable ↔ ∃ (g : E →ₗ.[R] F) (hg : g.is_closed), f ≤ g

The core of a linear operator #

source

structure linear_pmap.has_core {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] (f : E →ₗ.[R] F) (S : submodule R E) :

Prop

le_domain : S ≤ f.domain
closure_eq : (f.dom_restrict S).closure = f

A submodule S is a core of f if the closure of the restriction of f to S is again f.

source

theorem linear_pmap.has_core_def {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] {f : E →ₗ.[R] F} {S : submodule R E} (h : f.has_core S) :

(f.dom_restrict S).closure = f

source

theorem linear_pmap.closure_has_core {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] [has_continuous_add E] [has_continuous_add F] [topological_space R] [has_continuous_smul R E] [has_continuous_smul R F] (f : E →ₗ.[R] F) :

f.closure.has_core f.domain

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.