View source for Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Differentiation

== The Derivative of a Real Function ==

'''5.1 Definition'''<br/>
Mizar does not introduce differentiation via <math>\phi(t)</math> as Rudin does, but works directly with linear and rest functions (see <tt>FDIFF_1:def 2/3</tt>). There is no reference associating the Mizar differentiation with the notation of <tt>LIMFUNC3</tt>, but there are <tt>FDIFF_1:12</tt> and <tt>FDIFF_2:49</tt>. (On a side note, Mizar differentiation is not restricted to intervals <math>[a,b]</math>.)<br/>
<math>f</math> is differentiable at <math>x</math> means <tt>f is_differentiable_in x</tt> (<tt>FDIFF_1:def 4</tt>), <math>f'(x)</math> is <tt>diff(f,x)</tt> (<tt>FDIFF_1:def 5</tt>). <math>f</math> is differentiable on <math>E</math> means <tt>f is_differentiable_on E</tt> (<tt>FDIFF_1:def 6</tt>), <math>f'</math> is <tt>f`|E</tt> (<tt>FDIFF_1:def 7</tt>). See also <tt>FDIFF_1:def 8</tt> and <tt>POLYDIFF:def 1</tt>.<br/>
One-side differentiation is covered in <tt>FDIFF_3</tt>.

'''5.2 Theorem''' is <tt>FDIFF_1:24/25</tt>

'''5.3 Theorem'''<br/>
(a) is <tt>FDIFF_1:13/18</tt> or <tt>POLYDIFF:14</tt>.<br/> 
(b) is <tt>FDIFF_1:16/21</tt> or <tt>POLYDIFF:16</tt>.<br/>
(c) is <tt>FDIFF_2:14/21</tt>.

'''5.4 Examples'''<br/>
<math>c'=0</math> for constant <math>c</math> is <tt>FDIFF_1:11/22</tt>, see also <tt>POLYDIFF:11</tt>.<br/>
<math>x'=1</math> is <tt>FDIFF_1:17</tt>, see also <tt>POLYDIFF:12</tt>, and more general <math>(ax+b)'=a</math> is <tt>FDIFF_1:23</tt>.<br/>
Differentiation of polynomials is given by <tt>POLYDIFF:def 5/6</tt> and <tt>POLYDIFF:61</tt>. The notations seems a little bit sophisticated because polynomials have quite some structure behind them in Mizar, see <tt>PRE_POLY</tt> and the <tt>POLYNOM</tt> series.

'''5.5 Theorem''' is <tt>FDIFF_2:23</tt>.

'''5.6 Examples'''<br/>
(a) is <tt>FDIFF_5:7</tt>.<br/>
(b) is <tt>FDIFF_5:17</tt>, although <math>f'(0)</math> has been explicitly excluded, no reference for that.

== Mean Value Theorems ==

'''5.7 Definition''' No reference.

'''5.8 Theorem''' No reference, although the statement is basically proven within the proof of <tt>ROLLE:1</tt>. #TODO Explicit reference that local extrema of differentiable functions have derivation 0.

'''5.9 Theorem''' is <tt>ROLLE:5</tt>.

'''5.10 Theorem''' is <tt>ROLLE:3</tt>.

'''5.11 Theorem'''<br/>
(a) is <tt>ROLLE:11</tt> or <tt>FDIFF_2:31</tt>.<br/>
(b) is <tt>ROLLE:7</tt>.<br/>
(c) is <tt>ROLLE:12</tt> or <tt>FDIFF_2:32</tt>.

== The Continuity of Derivatives ==

'''5.12 Theorem''' No reference. #TODO <math>f'(a)<\lambda< f'(b)</math> implies the existence of an <math>x</math> such that <math>f'(x)=\lambda</math>.

'''Corollary''' No reference.

== L'Hospital's Rule ==

'''5.13 Theorem''' in <tt>L_HOSPIT</tt>, especially <tt>L_HOSPIT:10</tt>.

== Derivatives of Higher Order ==

'''5.14 Definition'''<br/>
<math>f^{(n)}</math> is <tt>diff(f,E).n</tt> (<tt>TAYLOR_1:def 5</tt>, see also <tt>TAYLOR_1:def 6</tt>), where <math>E</math> is the domain on which <math>f^{(n)}</math> is defined.

== Taylor's Theorem ==

'''5.15 Theorem'''<br/>
Set <math>c=\alpha</math> and <math>d=\beta</math>, then <math>P(t)</math> is <tt>Partial_Sums(Taylor(f,E,c,d)).(n-'1)</tt> (see <tt>SERIES_1:def 1</tt> and <tt>TAYLOR_1:def 7</tt>), where <math>E</math> is the domain on which <math>f^{(n)}</math> is defined. The theorem is <tt>TAYLOR_1:27</tt> with <math>n+1</math> instead of <math>n</math>.

== Differentiation of vector-valued Functions ==

'''5.16 Remark (about complex-valued functions)'''<br/>
Differentiation of functions from a subset of the reals to the complex are not formalized in Mizar, but definitions for complex differentiation are given by <tt>CFDIFF_1:def 6-9</tt> and <tt>CFDIFF_1:def 12</tt>, see also <tt>CFDIFF_1:22</tt>. Continuity of differentiable complex functions is given by <tt>CFDIFF_1:34/35</tt>. The differentiation rules <math>f+g</math> and <math>fg</math> are given by <tt>CFDIFF_1:23/28</tt>, <tt>CFDIFF_1:26/31</tt> respectively. No reference for <math>f/g</math>.

'''5.16 Remark (about normed spaces)'''<br/>
In <tt>NDIFF_1</tt> differentiation is defined between normed linear spaces (see <tt>NDIFF_1:def 6-9</tt>), i.e. the domain doesn't need to be a subset of the real numbers. No reference for differentiability iff the components are differentiable. See also <tt>PDIFF_1</tt>.<br/>
That differentiability implies continuity is given by <tt>NDIFF_1:44/45</tt>.<br/>
<math>f+g</math> is given by <tt>NDIFF_1:35/39</tt>. No reference for inner product.

'''5.16 Remark (about vector-valued functions)'''<br/>
For definitions see <tt>NDIFF_3:def 3-7</tt>, see also <tt>NDIFF_3:13</tt>. No reference for differentiability iff the components are differentiable. See also <tt>NDIFF_4</tt>.<br/>
That differentiability implies continuity is given by <tt>NDIFF_3:22/23</tt>.<br/>
<math>f+g</math> is given by <tt>NDIFF_3:14/17</tt>. No reference for inner product.

'''5.17 Examples''' No reference. <math>e^z</math> is defined in <tt>SIN_COS:def 14</tt>, <math>e^{ix}</math> is given by <tt>SIN_COS:25</tt>.

'''5.18 Examples''' No reference.

'''5.19 Theorem''' No reference.

== Exercises ==
1. is <tt>FDIFF_2:25</tt>.<br/>
2. is <tt>FDIFF_2:37/38</tt> or <tt>FDIFF_2:45</tt>.<br/>
3. No reference.<br/>
4. No reference.<br/>
5. No reference.<br/>
6. No reference.<br/>
7. see <tt>L_HOSPIT:10</tt>.<br/>
8. No reference.<br/>
9. No reference.<br/>
10. No reference.<br/>
11. No reference.<br/>
12. No reference.<br/>
13. No reference.<br/>
14. No reference.<br/>
15. No reference.<br/>
16. No reference.<br/>
17. No reference.<br/>
18. No reference.<br/>
19. No reference.<br/>
20. No reference.<br/>
21. No reference.<br/>
22. No reference.<br/>
23. No reference.<br/>
24. No reference.<br/>
25. No reference.<br/>
26. No reference. #TODO Find reference that <math>|f(x)|\leq A|f'(x)|</math> implies <math>f=0</math>.<br/>
27. No reference. #TODO Find reference for initial value problem.<br/>
28. No reference. #TODO Find reference for initial value problem.<br/>
29. No reference.

{{BookCat}}