<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>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 ||ƒ'(<italic>x</italic> + <italic>t</italic> · <italic>h</italic>)|| is bounded for <italic>t</italic> between 0 and 1 by some constant <italic>M</italic>, then ||ƒ(<italic>x</italic> + <italic>t</italic> · <italic>h</italic>) - ƒ(<italic>x</italic>)|| ≤ <italic>M</italic> · ||<italic>h</italic>||. 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].</p></abstract>

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

Differentiable Functions on Normed Linear Spaces

Formalized Mathematics

{"article-title":"Differentiable Functions on Normed Linear Spaces"}

In this article, we formalize differentiability of functions on normed linear spaces. Partial derivative, mean value theorem for vector-valued functions,...

Differentiable Functions on Normed Linear Spaces

Publié en ligne: 12 sept. 2012

Pages: 31 - 40

DOI: https://doi.org/10.2478/v10037-012-0005-1

This content is open access.