W BIAŁYMSTOKU
Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/17774Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Okazaki, Hiroyuki | - |
| dc.date.accessioned | 2025-01-03T09:47:00Z | - |
| dc.date.available | 2025-01-03T09:47:00Z | - |
| dc.date.issued | 2024 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 32, Issue 1, Pages 133–139 | pl |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/17774 | - |
| dc.description.abstract | In this study we are formalizing the optimization theory in Mizar. It is well known that geometric principles of linear vector space theory play fundamental roles in optimization. This article focuses on formalization of definitions and some theorems about dual spaces: we formalize orthogonal complements of real normed spaces, then we deal with minimum norm problems. | pl |
| dc.language.iso | en | pl |
| dc.publisher | DeGruyter Open | pl |
| dc.rights | Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0) | pl |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/3.0/ | pl |
| dc.subject | dual space | pl |
| dc.subject | orthonormal complement | pl |
| dc.subject | minimum norm problem | pl |
| dc.title | Formalization of Orthogonal Complements of Normed Spaces | pl |
| dc.type | Article | pl |
| dc.rights.holder | © 2024 The Author(s) | pl |
| dc.rights.holder | CC BY-SA 3.0 license | pl |
| dc.identifier.doi | 10.2478/forma-2024-0010 | - |
| dc.description.Affiliation | Shinshu University, Nagano, Japan | pl |
| dc.description.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. | pl |
| dc.description.references | Sylvie Boldo, Fran¸cois Cl´ement, 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. | pl |
| dc.description.references | 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. | pl |
| dc.description.references | Johannes Holzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279–294. Springer, 2013. | pl |
| dc.description.references | 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. | pl |
| dc.description.references | David G. Luenberger. Optimization by Vector Space Methods. John Wiley and Sons, 1969. | pl |
| dc.description.references | 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. | pl |
| dc.description.references | Louis Nirenberg. Functional Analysis: Lectures Given in 1960–61. Notes by Lesley Sibner. New York University, 1961. | pl |
| dc.description.references | 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. | pl |
| dc.description.references | Hiroyuki Okazaki. Formalization of orthogonal decomposition for Hilbert spaces. Formalized Mathematics, 30(4):295–299, 2022. doi:10.2478/forma-2022-0023. | pl |
| dc.description.references | 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. | pl |
| dc.description.references | Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991. | pl |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 32 | pl |
| dc.description.issue | 1 | pl |
| dc.description.firstpage | 133 | pl |
| dc.description.lastpage | 139 | pl |
| dc.identifier.citation2 | Formalized Mathematics | pl |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2024, Volume 32, Issue 1 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| Formalization-of-Orthogonal-Complements-of-Normed-Spaces.pdf | 247,52 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
