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.
Takao Inoué, Adam Naumowicz, Noboru Endou, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article, we define and develop partial differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [19] and [20]).
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).
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].
Takao Inoué, Noboru Endou, Yasunari Shidama (2010)
Formalized Mathematics
Similarity:
In this article, we define and develop differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [16] and [17]).
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...
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].
Takao Inoué, Adam Naumowicz, Noboru Endou, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article, we aim to prove the characterization of differentiation by means of partial differentiation for vector-valued functions on n-dimensional real normed linear spaces (refer to [15] and [16]).
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).
Haddad, Lucien, Lau, Dietlinde (2007)
Beiträge zur Algebra und Geometrie
Similarity:
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.