### Abstract

We present a formalization of bounded operators on complex vector
spaces. Our formalization contains material on complex vector spaces
(normed spaces, Banach spaces, Hilbert spaces) that complements and
goes beyond the developments of real vectors spaces in the
Isabelle/HOL standard library. We define the type of bounded
operators between complex vector spaces
(

BSD License*cblinfun*) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the Jordan_Normal_Form AFP entry.### Used by

### Topics

### Theories

- Extra_General
- Extra_Vector_Spaces
- Extra_Ordered_Fields
- Extra_Lattice
- Complex_Vector_Spaces0
- Complex_Vector_Spaces
- Complex_Inner_Product0
- Complex_Inner_Product
- Extra_Operator_Norm
- One_Dimensional_Spaces
- Complex_Euclidean_Space0
- Complex_Bounded_Linear_Function0
- Complex_Bounded_Linear_Function
- Extra_Infinite_Set_Sum
- Complex_L2
- Extra_Jordan_Normal_Form
- Cblinfun_Matrix
- Cblinfun_Code
- Extra_Pretty_Code_Examples
- Cblinfun_Code_Examples