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.

翻译：我们在Isabelle/HOL中提出了复向量空间上有界算子的形式化。我们的形式化包含复向量空间（赋范空间、巴拿赫空间、希尔伯特空间）的内容，补充并超越了Isabelle/HOL标准库中实向量空间的发展。我们定义了复向量空间之间有界算子的类型（cblinfun），并发展了酉算子、投影算子、有界线性函数延拓（BLT定理）、伴随算子、Loewner序、闭子空间等理论。对于有限维情形，我们通过将有限维算子与Jordan_Normal_Form AFP条目中形式化的矩阵进行等同，提供了代码生成支持。