DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.3

Complex Bounded Operators in Isabelle/HOL

Authors: Dominique Unruh and José Manuel Rodríguez Caballero

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

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, 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.

Cite as

Dominique Unruh and José Manuel Rodríguez Caballero. Complex Bounded Operators in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{unruh_et_al:LIPIcs.ITP.2026.3,
  author =	{Unruh, Dominique and Caballero, Jos\'{e} Manuel Rodr{\'\i}guez},
  title =	{{Complex Bounded Operators in Isabelle/HOL}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.3},
  URN =		{urn:nbn:de:0030-drops-269772},
  doi =		{10.4230/LIPIcs.ITP.2026.3},
  annote =	{Keywords: Formalized mathematics, functional analysis, bounded operators}
}

Search Results

Documents authored by Caballero, José Manuel Rodríguez

Complex Bounded Operators in Isabelle/HOL

Abstract

Cite as

Thanks for your feedback!

Could not send message