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).
Bing Xie, Xiquan Liang, Hongwei Li (2008)
Formalized Mathematics
Similarity:
In this article, we define two single-variable functions SVF1 and SVF2, then discuss partial differentiation of real binary functions by dint of one variable function SVF1 and SVF2. The main properties of partial differentiation are shown [7].MML identifier: PDIFF 2, version: 7.9.03 4.104.1021
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).
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].
Bing Xie, Xiquan Liang, Xiuzhuan Shen (2009)
Formalized Mathematics
Similarity:
In this article we define second-order partial differentiation of real binary functions and discuss the relation of second-order partial derivatives and partial derivatives defined in [17].
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.
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].
Keiko Narita, Artur Kornilowicz, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article we demonstrate basic properties of the continuous functions from R to Rn which correspond to state space equations in control engineering.
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]).
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]).
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.