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

The Derivative of a Real Function.
5.1 Definition
Mizar does not introduce differentiation via formula_1 as Rudin does, but works directly with linear and rest functions (see FDIFF_1:def 2/3). There is no reference associating the Mizar differentiation with the notation of LIMFUNC3, but there are FDIFF_1:12 and FDIFF_2:49. (On a side note, Mizar differentiation is not restricted to intervals formula_2.)
formula_3 is differentiable at formula_4 means f is_differentiable_in x (FDIFF_1:def 4), formula_5 is diff(f,x) (FDIFF_1:def 5). formula_3 is differentiable on formula_7 means f is_differentiable_on E (FDIFF_1:def 6), formula_8 is f`|E (FDIFF_1:def 7). See also FDIFF_1:def 8 and POLYDIFF:def 1.
One-side differentiation is covered in FDIFF_3.
5.2 Theorem is FDIFF_1:24/25
5.3 Theorem
(a) is FDIFF_1:13/18 or POLYDIFF:14. 
(b) is FDIFF_1:16/21 or POLYDIFF:16.
(c) is FDIFF_2:14/21.
5.4 Examples
formula_9 for constant formula_10 is FDIFF_1:11/22, see also POLYDIFF:11.
formula_11 is FDIFF_1:17, see also POLYDIFF:12, and more general formula_12 is FDIFF_1:23.
Differentiation of polynomials is given by POLYDIFF:def 5/6 and POLYDIFF:61. The notations seems a little bit sophisticated because polynomials have quite some structure behind them in Mizar, see PRE_POLY and the POLYNOM series.
5.5 Theorem is FDIFF_2:23.
5.6 Examples
(a) is FDIFF_5:7.
(b) is FDIFF_5:17, although formula_13 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 ROLLE:1. #TODO Explicit reference that local extrema of differentiable functions have derivation 0.
5.9 Theorem is ROLLE:5.
5.10 Theorem is ROLLE:3.
5.11 Theorem
(a) is ROLLE:11 or FDIFF_2:31.
(b) is ROLLE:7.
(c) is ROLLE:12 or FDIFF_2:32.
The Continuity of Derivatives.
5.12 Theorem No reference. #TODO formula_14 implies the existence of an formula_4 such that formula_16.
Corollary No reference.
L'Hospital's Rule.
5.13 Theorem in L_HOSPIT, especially L_HOSPIT:10.
Derivatives of Higher Order.
5.14 Definition
formula_17 is diff(f,E).n (TAYLOR_1:def 5, see also TAYLOR_1:def 6), where formula_7 is the domain on which formula_17 is defined.
Taylor's Theorem.
5.15 Theorem
Set formula_20 and formula_21, then formula_22 is Partial_Sums(Taylor(f,E,c,d)).(n-'1) (see SERIES_1:def 1 and TAYLOR_1:def 7), where formula_7 is the domain on which formula_17 is defined. The theorem is TAYLOR_1:27 with formula_25 instead of formula_26.
Differentiation of vector-valued Functions.
5.16 Remark (about complex-valued functions)
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 CFDIFF_1:def 6-9 and CFDIFF_1:def 12, see also CFDIFF_1:22. Continuity of differentiable complex functions is given by CFDIFF_1:34/35. The differentiation rules formula_27 and formula_28 are given by CFDIFF_1:23/28, CFDIFF_1:26/31 respectively. No reference for formula_29.
5.16 Remark (about normed spaces)
In NDIFF_1 differentiation is defined between normed linear spaces (see NDIFF_1:def 6-9), 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 PDIFF_1.
That differentiability implies continuity is given by NDIFF_1:44/45.
formula_27 is given by NDIFF_1:35/39. No reference for inner product.
5.16 Remark (about vector-valued functions)
For definitions see NDIFF_3:def 3-7, see also NDIFF_3:13. No reference for differentiability iff the components are differentiable. See also NDIFF_4.
That differentiability implies continuity is given by NDIFF_3:22/23.
formula_27 is given by NDIFF_3:14/17. No reference for inner product.
5.17 Examples No reference. formula_32 is defined in SIN_COS:def 14, formula_33 is given by SIN_COS:25.
5.18 Examples No reference.
5.19 Theorem No reference.
Exercises.
1. is FDIFF_2:25.
2. is FDIFF_2:37/38 or FDIFF_2:45.
3. No reference.
4. No reference.
5. No reference.
6. No reference.
7. see L_HOSPIT:10.
8. No reference.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference.
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference.
20. No reference.
21. No reference.
22. No reference.
23. No reference.
24. No reference.
25. No reference.
26. No reference. #TODO Find reference that formula_34 implies formula_35.
27. No reference. #TODO Find reference for initial value problem.
28. No reference. #TODO Find reference for initial value problem.
29. No reference.