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.
翻译：泛函分析，特别是希尔伯特空间及其上算子理论，是数学中的重要领域。我们形式化了Isabelle/HOL库Complex_Bounded_Operators，其中包含大量关于复希尔伯特空间及其上（有界）算子的定理。具体而言，我们形式化了复向量空间、内积（及希尔伯特）空间、一维空间、有界算子、伴随算子、酉算子、投影算子、有界算子的延拓（BLT定理）、正算子、平方可和序列等诸多性质。此外，我们为有限维情形提供了代码生成支持。
相关内容
微信扫码咨询专知VIP会员