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

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Complex_Bounded_Operators

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

### Session Complex_Bounded_Operators_Dependencies

### Depends on

- Banach-Steinhaus Theorem
- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Implementing field extensions of the form Q[sqrt(b)]

### Used by

- Quantum and Classical Registers

## Cite

×

Complex_Bounded_Operators-AFP

    @article{Complex_Bounded_Operators-AFP,
      author  = {José Manuel Rodríguez Caballero and Dominique Unruh},
      title   = {Complex Bounded Operators},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Complex_Bounded_Operators.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Sep 20, 2021 : Isabelle2021