Implicit Function Theorem. Part II

Kazuhisa Nakasho; Yasunari Shidama

doi:10.2478/forma-2019-0013

.blurhash-client-img { display: none !important; }

Implicit Function Theorem. Part II

Formalized Mathematics

Volume 27 (2019): Issue 2 (July 2019)

By: Kazuhisa Nakasho and Yasunari Shidama

Open Access

|Jul 2019

Abstract

In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum decomposition of Lipschitz continuous linear operator are mentioned here.

In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.

References

[1] 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.10.1007/s10817-017-9440-6604425130069070
Open DOI Search in Google Scholar Back to article
[2] Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.
Search in Google Scholar Back to article
[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.10.1007/s10817-015-9345-1
Open DOI Search in Google Scholar Back to article
[4] Hiroshi Imura, Morishige Kimura, and Yasunari Shidama. The differentiable functions on normed linear spaces. Formalized Mathematics, 12(3):321–327, 2004.
Search in Google Scholar Back to article
[5] Kazuhisa Nakasho. Invertible operators on Banach spaces. Formalized Mathematics, 27 (2):107–115, 2019. doi:10.2478/forma-2019-0012.10.2478/forma-2019-0012
Open DOI Search in Google Scholar Back to article
[6] Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026.10.1515/forma-2017-0026
Open DOI Search in Google Scholar Back to article
[7] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004.
Search in Google Scholar Back to article
[8] 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.10.2478/v10037-011-0009-2
Search in Google Scholar Back to article
[9] Hideki Sakurai, Hiroyuki Okazaki, and Yasunari Shidama. Banach’s continuous inverse theorem and closed graph theorem. Formalized Mathematics, 20(4):271–274, 2012. doi:10.2478/v10037-012-0032-y.10.2478/v10037-012-0032-y
Open DOI Search in Google Scholar Back to article
[10] Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.
Search in Google Scholar Back to article
[11] Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/forma-2019-0013 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 117 - 131

Accepted on: May 27, 2019

Published on: Jul 20, 2019

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

implicit function theorem,

Lipschitz continuity,

Related subjects:

Computer sciences, other

© 2019 Kazuhisa Nakasho, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.

Volume 27 (2019): Issue 2 (July 2019)