Complex Bounded Operators in Isabelle/HOL
Dominique Unruh, Jos\'e Manuel Rodr\'iguez Caballero
TL;DR
This paper presents a formalization of complex bounded operators in Isabelle/HOL, covering key theorems and properties of Hilbert spaces and operators, with support for finite-dimensional code generation.
Contribution
It introduces a comprehensive Isabelle/HOL library formalizing complex Hilbert spaces and bounded operators, including the BLT-theorem and code generation capabilities.
Findings
Formalized core theorems of complex Hilbert spaces
Supported code generation for finite-dimensional cases
Enhanced Isabelle/HOL library for functional analysis
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAlgebraic and Geometric Analysis · Mathematical and Theoretical Analysis · Advanced Algebra and Logic