Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces

Pole DC	Wartość	Język
dc.contributor.author	Nakasho, Kazuhisa	-
dc.contributor.author	Shidama, Yasunari	-
dc.date.accessioned	2025-01-10T10:28:41Z	-
dc.date.available	2025-01-10T10:28:41Z	-
dc.date.issued	2024	-
dc.identifier.citation	Formalized Mathematics, Volume 32, Issue 1, Pages 247–269	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/17801	-
dc.description.abstract	This article extends the formalization of the theory of differentiation in real normed spaces in the Mizar system. The focus is on higher-order derivatives and the inverse function theorem. Additionally, we encode the differentiability of the inversion operator on invertible linear operators.	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	higher-order derivative	pl
dc.subject	inverse function theorem	pl
dc.subject	real normed space	pl
dc.subject	vector-valued function	pl
dc.title	Higher-Order Differentiation and Inverse Function Theorem in Real 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-0021	-
dc.description.Affiliation	Kazuhisa Nakasho - Yamaguchi University, Yamaguchi, Japan	pl
dc.description.Affiliation	Yasunari Shidama - Karuizawa Hotch 244-1, 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 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.	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	Nelson Dunford and Jacob T. Schwartz. Linear operators I. Interscience Publ., 1958.	pl
dc.description.references	Noboru Endou and Yasunari Shidama. Differentiation in normed spaces. Formalized Mathematics, 21(2):95–102, 2013. doi:10.2478/forma-2013-0011.	pl
dc.description.references	Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972.	pl
dc.description.references	Kazuhisa Nakasho. Invertible operators on Banach spaces. Formalized Mathematics, 27 (2):107–115, 2019. doi:10.2478/forma-2019-0012.	pl
dc.description.references	Kazuhisa Nakasho and Yasunari Shidama. On implicit and inverse function theorems on Euclidean spaces. Formalized Mathematics, 30(3):159–168, 2022. doi:10.2478/forma-2022-0012	pl
dc.description.references	Kazuhisa Nakasho and Yasunari Shidama. Differentiability properties of Lipschitzian bilinear operators in real normed spaces. Formalized Mathematics, 32(1):165–172, 2024.doi:10.2478/forma-2024-0013.	pl
dc.description.references	Hiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of family of real linear spaces. Formalized Mathematics, 19(1):51–59, 2011. doi:10.2478/v10037-011-0009-2.	pl
dc.description.references	Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.	pl
dc.description.references	Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.	pl
dc.description.references	Kôsaku Yosida. Functional Analysis. Springer, 1980.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	32	pl
dc.description.issue	1	pl
dc.description.firstpage	247	pl
dc.description.lastpage	269	pl
dc.identifier.citation2	Formalized Mathematics	pl
dc.identifier.orcid	0000-0003-1110-4342	-
Występuje w kolekcji(ach):	Formalized Mathematics, 2024, Volume 32, Issue 1

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
HigherOrder-Differentiation-and-Inverse-Function-Theorem-in-Real-Normed-Spaces.pdf		339,23 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

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