The continuous functional calculus in Lean
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913666764374016 |
|---|---|
| author | Dedecker, Anatole Loreaux, Jireh |
| author_facet | Dedecker, Anatole Loreaux, Jireh |
| contents | The continuous functional calculus is perhaps the most fundamental construction in the theory of operator algebras, especially $C^{*}$-algebras. Here we document our formalization of the continuous functional calculus in Lean, which constitutes the first such formalization in any proof assistant. Our implementation is already merged into Lean's mathematical library, Mathlib. We provide a brief introduction to the mathematical theory for those unfamiliar with the subject, and then highlight the design decisions in our formalization which proved to be important for usability. Our exposition is aimed at a general mathematical audience and provides a glimpse into the world of formalization by laying bare the discovery process. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_15639 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The continuous functional calculus in Lean Dedecker, Anatole Loreaux, Jireh Operator Algebras Logic in Computer Science 68V20 (Primary) 47B15, 46L05, 68V35 (Secondary) The continuous functional calculus is perhaps the most fundamental construction in the theory of operator algebras, especially $C^{*}$-algebras. Here we document our formalization of the continuous functional calculus in Lean, which constitutes the first such formalization in any proof assistant. Our implementation is already merged into Lean's mathematical library, Mathlib. We provide a brief introduction to the mathematical theory for those unfamiliar with the subject, and then highlight the design decisions in our formalization which proved to be important for usability. Our exposition is aimed at a general mathematical audience and provides a glimpse into the world of formalization by laying bare the discovery process. |
| title | The continuous functional calculus in Lean |
| topic | Operator Algebras Logic in Computer Science 68V20 (Primary) 47B15, 46L05, 68V35 (Secondary) |
| url | https://arxiv.org/abs/2501.15639 |