References
- Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: a survey of proof assistants and libraries. Mathematical Structures in Computer Science, pages 1–38, 2014.
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79–89, New York, NY, USA, 2017. Association for Computing Machinery. doi:10.1145/3018610.3018625.
- Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.
- Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279–294. Springer, 2013.
- Chenyi Li, Ziyu Wang, Wanyi He, Yuxuan Wu, Shengyang Xu, and Zaiwen Wen. Formalization of complexity analysis of the first-order algorithms for convex optimization. arXiv preprint arXiv:2403.11437, 2024.
- David G. Luenberger. Optimization by Vector Space Methods. John Wiley and Sons, 1969.
- Keiko Narita, Noboru Endou, and Yasunari Shidama. Dual spaces and Hahn-Banach theorem. Formalized Mathematics, 22(1):69–77, 2014. doi:10.2478/forma-2014-0007.
- Louis Nirenberg. Functional Analysis: Lectures Given in 1960–61. Notes by Lesley Sibner. New York University, 1961.
- Hiroyuki Okazaki. On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors. Formalized Mathematics, 31(1):53–57, 2023. doi:10.2478/forma-2023-0005.
- Hiroyuki Okazaki. Formalization of orthogonal decomposition for Hilbert spaces. Formalized Mathematics, 30(4):295–299, 2022. doi:10.2478/forma-2022-0023.
- Colin Rothgang, Artur Korniłowicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 205–210, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81097-9 17.
- Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
Language: English
Page range: 133 - 139
Submitted on: Nov 28, 2024
Published on: Dec 31, 2024
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Keywords:
Related subjects:
© 2024 Hiroyuki Okazaki, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.