Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Complex Bounded Operators

Email Gateway (Sep 20 2021 at 08:02):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce a new entry in the AFP.

Enjoy,
René

Complex Bounded Operators
by Jose Manuel Rodriguez Caballero and Dominique Unruh

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.

https://www.isa-afp.org/entries/Complex_Bounded_Operators.html

Last updated: Apr 25 2024 at 12:23 UTC