%0 Journal Article
%T Differentiable Functions on Normed Linear Spaces
%A Yasunari Shidama
%J Formalized Mathematics
%@ 1898-9934
%D 2012
%I 
%R 10.2478/v10037-012-0005-1
%X 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 M, then || (x + t ¡¤ h) -  (x)|| ¡Ü M ¡¤ ||h||. This theorem is called the mean value theorem for vector-valued functions. By this theorem, the relation between the (total) derivative and the partial derivatives of a function is derived [23].
%U http://versita.metapress.com/content/456x4m1582655581/?p=430716bb19384440aaea6ce45ed7408d&pi=4