Complex Bounded Operators in Isabelle/HOL

2025/12/05 by Unruh, Dominique, Caballero, José Manuel Rodríguez
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2512.05878

Abstract

Functional analysis, especially the theory of Hilbert spaces and of operators on these, form an important area in mathematics. We formalized the Isabelle/HOL library Complex_Bounded_Operators containing a large amount of theorems about complex Hilbert spaces and (bounded) operators on these. Specifically, we formalize the properties complex vector spaces, inner product (and Hilbert) spaces, one-dimensional spaces, bounded operators, adjoints, unitaries, projections, extensions of bounded operators (BLT-theorem), positive operators, square-summable sequences and much more. Additionally, we provide support for code generation in the finite-dimensional case.

Citations

• Quantum references
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
• Runtime Analysis of Quantum Programs: A Formal Approach
• Quantum Temporal Logic
• Model checking quantum Markov chains
• Termination of Nondeterministic Quantum Programs
• Floyd--hoare logic for quantum programs

Related

• Functional Analysis and Operator Theory
• On unbounded complementable operators
• Inner functions and operator theory
• The Bishop-Phelps-Bollobás properties in complex Hilbert spaces
• Diagonals of operators and Blaschke's enigma