Displaying similar documents to “Differentiable Functions into Real Normed Spaces”

Differentiable Functions on Normed Linear Spaces

Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article, we formalize differentiability of functions on normed linear spaces. Partial derivative, mean value theorem for vector-valued functions, continuous differentiability, etc. are formalized. As it is well known, there is no exact analog of the mean value theorem for vector-valued functions. However a certain type of generalization of the mean value theorem for vector-valued functions is obtained as follows: If ||ƒ'(x + t · h)|| is bounded for t between 0 and 1 by some constant...

Complex Function Differentiability

Chanapat Pacharapokin, Hiroshi Yamazaki, Yasunari Shidama, Yatsuka Nakamura (2009)

Formalized Mathematics

Similarity:

For a complex valued function defined on its domain in complex numbers the differentiability in a single point and on a subset of the domain is presented. The main elements of differential calculus are developed. The algebraic properties of differential complex functions are shown.

More on Continuous Functions on Normed Linear Spaces

Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama (2011)

Formalized Mathematics

Similarity:

In this article we formalize the definition and some facts about continuous functions from R into normed linear spaces [14].

Contracting Mapping on Normed Linear Space

Keiichi Miyajima, Artur Korniłowicz, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article, we described the contracting mapping on normed linear space. Furthermore, we applied that mapping to ordinary differential equations on real normed space. Our method is based on the one presented by Schwarz [29].

Higher-Order Partial Differentiation

Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article, we shall extend the formalization of [10] to discuss higher-order partial differentiation of real valued functions. The linearity of this operator is also proved (refer to [10], [12] and [13] for partial differentiation).

Differentiation in Normed Spaces

Noboru Endou, Yasunari Shidama (2013)

Formalized Mathematics

Similarity:

In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces [14].

The Differentiable Functions from R into R n

Keiko Narita, Artur Korniłowicz, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In control engineering, differentiable partial functions from R into Rn play a very important role. In this article, we formalized basic properties of such functions.

The C k Space

Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama (2013)

Formalized Mathematics

Similarity:

In this article, we formalize continuous differentiability of realvalued functions on n-dimensional real normed linear spaces. Next, we give a definition of the Ck space according to [23].

Partial Differentiation of Real Ternary Functions

Takao Inoué, Bing Xie, Xiquan Liang (2010)

Formalized Mathematics

Similarity:

In this article, we shall extend the result of [19] to discuss partial differentiation of real ternary functions (refer to [8] and [16] for partial differentiation).