F. Riesz Theorem

Pole DC	Wartość	Język
dc.contributor.author	Narita, Keiko	-
dc.contributor.author	Nakasho, Kazuhisa	-
dc.contributor.author	Shidama, Yasunari	-
dc.date.accessioned	2018-02-08T08:13:52Z	-
dc.date.available	2018-02-08T08:13:52Z	-
dc.date.issued	2017	-
dc.identifier.citation	Formalized Mathematics, Volume 25, Issue 3, Pages 179–184	-
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/6292	-
dc.description.abstract	SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor ClstoCmp, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [10] and the article [5], we defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties.In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [7], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [8] and the article [6]. These formalizations are based on [2], [3], [9], and [11].	-
dc.language.iso	en	-
dc.publisher	DeGruyter Open	-
dc.subject	F. Riesz theorem	-
dc.subject	dual spaces	-
dc.subject	continuous functions	-
dc.title	F. Riesz Theorem	-
dc.type	Article	-
dc.identifier.doi	10.1515/forma-2017-0017	-
dc.description.Affiliation	Narita Keiko - Hirosaki-city, Aomori, Japan	-
dc.description.Affiliation	Nakasho Kazuhisa - Akita Prefectural University, Akita, Japan	-
dc.description.Affiliation	Shidama Yasunari - Shinshu University, Nagano, Japan	-
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 and beyond. 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.	-
dc.description.references	Haim Brezis. Functional Analysis, Sobolev Spaces and Partial Differential Equations. Springer, 2011.	-
dc.description.references	Peter D. Dax. Functional Analysis. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley Interscience, 2002.	-
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.	-
dc.description.references	Katuhiko Kanazashi, Noboru Endou, and Yasunari Shidama. Banach algebra of continuous functionals and the space of real-valued continuous functionals with bounded support. Formalized Mathematics, 18(1):11–16, 2010. doi:10.2478/v10037-010-0002-1.	-
dc.description.references	Kazuhisa Nakasho, Keiko Narita, and Yasunari Shidama. The basic existence theorem of Riemann-Stieltjes integral. Formalized Mathematics, 24(4):253–259, 2016. doi:10.1515/forma-2016-0021.	-
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.	-
dc.description.references	Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. Riemann-Stieltjes integral. Formalized Mathematics, 24(3):199–204, 2016. doi:10.1515/forma-2016-0016.	-
dc.description.references	Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.	-
dc.description.references	Yasunari Shidama, Hikofumi Suzuki, and Noboru Endou. Banach algebra of bounded functionals. Formalized Mathematics, 16(2):115–122, 2008. doi:10.2478/v10037-008-0017-z.	-
dc.description.references	Kosaku Yoshida. Functional Analysis. Springer, 1980.	-
dc.identifier.eissn	1898-9934	-
dc.description.volume	25	-
dc.description.issue	3	-
dc.description.firstpage	179	-
dc.description.lastpage	184	-
dc.identifier.citation2	Formalized Mathematics	-
Występuje w kolekcji(ach):	Formalized Mathematics, 2017, Volume 25, Issue 3

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
forma-2017-0017.pdf		279,26 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

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