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
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].
Takao Inoué (2010)
Formalized Mathematics
Similarity:
In this article, we shall extend the result of [17] to discuss second-order partial differentiation of real ternary functions (refer to [7] and [14] for partial differentiation).
Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article, we formalize the differentiability of functions from the set of real numbers into a normed vector space [14].
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.
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).
Yuichi Futa, Noboru Endou, Yasunari Shidama (2013)
Formalized Mathematics
Similarity:
In this article, we formalize isometric differentiable functions on real normed space [17], and their properties.
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).
Hiroshi Yamazaki, Yasunari Shidama, Yatsuka Nakamura, Chanapat Pacharapokin (2009)
Formalized Mathematics
Similarity:
In this article we prove Cauchy-Riemann differential equations of complex functions. These theorems give necessary and sufficient condition for differentiable function.
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...
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].