Document Open Access Logo

Formalized functional analysis with semilinear maps

Authors Frédéric Dupuis , Robert Y. Lewis , Heather Macbeth

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2022.10.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Functional analysis
Keywords
  • Functional analysis
  • Lean
  • linear algebra
  • semilinear
  • Hilbert space

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean’s mathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fréchet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonné and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.

Cite As Get BibTex

Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ITP.2022.10

Author Details

Frédéric Dupuis
  • Département d'informatique et de recherche opérationnelle, University of Montr'eal, Canada
Robert Y. Lewis
  • Computer Science Department, Brown University, Providence, RI, USA
Heather Macbeth
  • Department of Mathematics, Fordham University, New York, NY, USA

Acknowledgements

We thank Johan Commelin for many conversations about isocrystals and Johannes Hölzl for comments on work in Isabelle. We thank the mathlib community and maintainer team for insightful comments and suggestions during code review.

Supplementary Materials

References

  1. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: A case study in functional analysis. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 3-20. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_1.
  2. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. J. Formalized Reasoning, 11(1):43-76, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8124.
  3. Sanaz Khan Afshar, Vincent Aravantinos, Osman Hasan, and Sofiène Tahar. Formalization of complex vectors in higher-order logic. In Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, and Josef Urban, editors, Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings, volume 8543 of Lecture Notes in Computer Science, pages 123-137. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08434-3_10.
  4. Jesús Aransay and Jose Divasón. Generalizing a mathematical analysis library in Isabelle/HOL. In Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, volume 9058 of Lecture Notes in Computer Science, pages 415-421. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-17524-9_30.
  5. Jesús Aransay and Jose Divasón. A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem. J. Autom. Reason., 58(4):509-535, April 2017. URL: https://doi.org/10.1007/s10817-016-9379-z.
  6. Anne Baanen. Use and abuse of instance parameters in the Lean mathematical library. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2022. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  7. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 79-89. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018625.
  8. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41-62, March 2015. URL: https://doi.org/10.1007/s11786-014-0181-1.
  9. Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified quantum computation in Isabelle/HOL. J. Autom. Reason., 65(5):691-709, 2021. URL: https://doi.org/10.1007/s10817-020-09584-7.
  10. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 299-312, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373830.
  11. Jose Manuel Rodriguez Caballero and Dominique Unruh. Complex bounded operators. Archive of Formal Proofs, September 2021. Formal proof development. URL: https://isa-afp.org/entries/Complex_Bounded_Operators.html.
  12. Johan Commelin and Robert Y. Lewis. Formalizing the ring of Witt vectors. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 264-277, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437992.3439919.
  13. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (system description). In Amy P. Felty and Aart Middeldorp, editors, CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. Google Scholar
  14. M. Demazure. Lectures on p-Divisible Groups. Lecture Notes in Mathematics. Springer Berlin Heidelberg, 2006. Google Scholar
  15. Sébastien Gouëzel. Lp spaces. Archive of Formal Proofs, October 2016. Formal proof development. URL: https://isa-afp.org/entries/Lp.html.
  16. John Harrison. The HOL Light theory of Euclidean space. J. Autom. Reason., 50(2):173-190, 2013. URL: https://doi.org/10.1007/s10817-012-9250-9.
  17. Michiel Hazewinkel. Witt vectors. Part 1. Handbook of Algebra, pages 319-472, 2009. URL: https://doi.org/10.1016/s1570-7954(08)00207-6.
  18. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 279-294. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  19. Yury Kudryashov. Formalizing the divergence theorem and the Cauchy integral formula in Lean. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2022. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  20. Peter Lammich and Andreas Lochbihler. Automatic refinement to efficient data structures: A comparison of two approaches. J. Autom. Reason., 63(1):53-94, 2019. URL: https://doi.org/10.1007/s10817-018-9461-9.
  21. Jacob Lurie. Lecture notes on the Fargues-Fontaine curve. Lecture 26: Isocrystals, December 2018. URL: https://www.math.ias.edu/~lurie/205notes/Lecture26-Isocrystals.pdf.
  22. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, November 2020. URL: https://doi.org/10.5281/zenodo.4282710.
  23. Mohamed Yousri Mahmoud, Vincent Aravantinos, and Sofiène Tahar. Formalization of infinite dimension linear spaces with application to quantum theory. In Guillaume Brat, Neha Rungta, and Arnaud Venet, editors, NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, volume 7871 of Lecture Notes in Computer Science, pages 413-427. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38088-4_28.
  24. Ju. I. Manin. Theory of commutative formal groups over fields of finite characteristic. Uspehi Mat. Nauk, 18(6 (114)):3-90, 1963. Google Scholar
  25. The mathlib Community. The Lean mathematical library. In CPP, pages 367-381, New York, NY, USA, 2020. ACM. URL: https://doi.org/10.1145/3372885.3373824.
  26. Keiko Narita, Noboru Endou, and Yasunari Shidama. The orthogonal projection and the Riesz representation theorem. Formaliz. Math., 23(3):243-252, 2015. URL: https://doi.org/10.1515/forma-2015-0020.
  27. Bas Spitters and Eelis van der Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21(4):795-825, 2011. URL: https://doi.org/10.1017/S0960129511000119.
  28. Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis. Maintaining a library of formal mathematics. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Mathematics, pages 251-267, Cham, 2020. Springer International Publishing. Google Scholar
  29. Eric Wieser. Scalar actions in Lean’s mathlib. CoRR, abs/2108.10700, 2021. URL: http://arxiv.org/abs/2108.10700.
  30. Niklaus Wirth. Program development by stepwise refinement. Commun. ACM, 14(4):221-227, April 1971. URL: https://doi.org/10.1145/362575.362577.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact