Displaying similar documents to “ The Differentiable Functions from R into R n ”

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].

Vector Functions and their Differentiation Formulas in 3-dimensional Euclidean Spaces

Xiquan Liang, Piqing Zhao, Ou Bai (2010)

Formalized Mathematics

Similarity:

In this article, we first extend several basic theorems of the operation of vector in 3-dimensional Euclidean spaces. Then three unit vectors: e1, e2, e3 and the definition of vector function in the same spaces are introduced. By dint of unit vector the main operation properties as well as the differentiation formulas of vector function are shown [12].

Differential Equations on Functions from R into Real Banach Space

Keiko Narita, Noboru Endou, Yasunari Shidama (2013)

Formalized Mathematics

Similarity:

In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations...

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].

An abstract nonlinear second order differential equation

Jan Bochenek (1991)

Annales Polonici Mathematici

Similarity:

By using the theory of strongly continuous cosine families of linear operators in Banach space the existence of solutions of a semilinear second order differential initial value problem (1) as well as the existence of solutions of the linear inhomogeneous problem corresponding to (1) are proved. The main result of the paper is contained in Theorem 5.