Complex Bounded Operators in Isabelle/HOL
Logic in Computer Science
2025-12-08 v1
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.
Cite
@article{arxiv.2512.05878,
title = {Complex Bounded Operators in Isabelle/HOL},
author = {Dominique Unruh and José Manuel Rodríguez Caballero},
journal= {arXiv preprint arXiv:2512.05878},
year = {2025}
}