Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complex Bounded Operators in Isabelle/HOL

Dominique Unruh, José Manuel Rodríguez Caballero

TL;DR

This work advances formal verification of functional analysis in Isabelle/HOL by developing a comprehensive library for complex Hilbert spaces and bounded operators, addressing infinite-dimensional settings relevant to quantum languages. The approach builds a structured ecosystem: complex vector spaces, inner products, conjugation, ℓ₂, and matrix-operator correspondences, all with code-generation support to enable computable reasoning in finite dimensions. Key contributions include the BLT extension tool, Riesz representation in operator form, a robust Loewner order for positive operators, and a detailed treatment of one-dimensional and finite-dimensional specializations that align with existing real-case libraries. The resulting framework enables rigorous, machine-checked reasoning about quantum programming formalisms and provides a scalable bridge to practical computation via code generation and matrix representations in finite dimensions.

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.

Complex Bounded Operators in Isabelle/HOL

TL;DR

This work advances formal verification of functional analysis in Isabelle/HOL by developing a comprehensive library for complex Hilbert spaces and bounded operators, addressing infinite-dimensional settings relevant to quantum languages. The approach builds a structured ecosystem: complex vector spaces, inner products, conjugation, ℓ₂, and matrix-operator correspondences, all with code-generation support to enable computable reasoning in finite dimensions. Key contributions include the BLT extension tool, Riesz representation in operator form, a robust Loewner order for positive operators, and a detailed treatment of one-dimensional and finite-dimensional specializations that align with existing real-case libraries. The resulting framework enables rigorous, machine-checked reasoning about quantum programming formalisms and provides a scalable bridge to practical computation via code generation and matrix representations in finite dimensions.

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.

Paper Structure

This paper contains 60 sections, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Overview of our contribution
  3. How to use this paper?
  4. Related work
  5. Preliminaries
  6. Mathematical background.
  7. Isabelle/HOL background.
  8. Complex vector spaces
  9. Type classes.
  10. Subspace, span, linear.
  11. Antilinear, sesquilinear, conjugate space.
  12. Finite-dimensional spaces.
  13. Closed subspaces.
  14. Product spaces.
  15. Inner product spaces
  16. ...and 45 more sections

Figures (1)

  • Figure 1: Number of (non-blank) lines of code, definitions, and proven facts in our development. extra/* summarizes all additional theories proving additional theorems (required by but not directly related to our formalization). Theories ending in 0 are analogous to existing Isabelle/HOL content for real vector spaces, the rest is fully new.