Formalization of Orthogonal Complements of Normed Spaces

[1] 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.Search in Google Scholar

[2] 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.Open DOISearch in Google Scholar

[3] 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.Open DOISearch in Google Scholar

[4] 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.Search in Google Scholar

[5] 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.Search in Google Scholar

[6] David G. Luenberger. Optimization by Vector Space Methods. John Wiley and Sons, 1969.Search in Google Scholar

[7] 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.Open DOISearch in Google Scholar

[8] Louis Nirenberg. Functional Analysis: Lectures Given in 1960–61. Notes by Lesley Sibner. New York University, 1961.Search in Google Scholar

[9] 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.Open DOISearch in Google Scholar

[10] Hiroyuki Okazaki. Formalization of orthogonal decomposition for Hilbert spaces. Formalized Mathematics, 30(4):295–299, 2022. doi:10.2478/forma-2022-0023.Open DOISearch in Google Scholar

[11] 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.Open DOISearch in Google Scholar

[12] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.Search in Google Scholar