Complex Bounded Operators in Isabelle/HOL

Dominique Unruh, José Manuel Rodríguez Caballero

We present a formalization of bounded operators on complex vector spaces in Isabelle/HOL. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces…