Formalization of Orthogonal Decomposition for Hilbert Spaces

Pole DC	Wartość	Język
dc.contributor.author	Okazaki, Hiroyuki	-
dc.date.accessioned	2023-02-27T13:08:43Z	-
dc.date.available	2023-02-27T13:08:43Z	-
dc.date.issued	2022	-
dc.identifier.citation	Formalized Mathematics, Volume 30, Issue 4, Pages 295-299	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/14708	-
dc.description.abstract	In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. For any subspace S of a Hilbert space H, any vector can be represented by the sum of a vectorin S and a vector orthogonal to S. The formalization of orthogonal complements of Hilbert spaces has been stored in the Mizar Mathematical Library [4]. We referred to [5] and [6] in the formalization.	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	Hilbert space	pl
dc.subject	orthogonal decomposition	pl
dc.subject	topological space	pl
dc.title	Formalization of Orthogonal Decomposition for Hilbert Spaces	pl
dc.type	Article	pl
dc.rights.holder	© 2022 The Author(s)	pl
dc.rights.holder	CC BY-SA 3.0 license	pl
dc.identifier.doi	10.2478/forma-2022-0023	-
dc.description.Affiliation	Hiroyuki Okazaki, Shinshu University, Nagano, Japan	pl
dc.description.references	Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art andeyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.	pl
dc.description.references	Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32,2018. doi:10.1007/s10817-017-9440-6.	pl
dc.description.references	Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Subspaces and cosets of subspace of real unitary space. Formalized Mathematics, 11(1):1–7, 2003.	pl
dc.description.references	Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Topology of real unitary space. Formalized Mathematics, 11(1):33–38, 2003.	pl
dc.description.references	David G. Luenberger. Optimization by Vector Space Methods. John Wiley and Sons, 1969.	pl
dc.description.references	Kôsaku Yosida. Functional Analysis. Springer, 1980.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	30	pl
dc.description.issue	4	pl
dc.description.firstpage	295	pl
dc.description.lastpage	299	pl
dc.identifier.citation2	Formalized Mathematics	pl
Występuje w kolekcji(ach):	Formalized Mathematics, 2022, Volume 30, Issue 4

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
10.2478_forma-2022-0023.pdf		224 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL