Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Differentiation
The Derivative of a Real Function edit
Mizar does not introduce differentiation via 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 .)
is differentiable at means f is_differentiable_in x (FDIFF_1:def 4), is diff(f,x) (FDIFF_1:def 5). is differentiable on means f is_differentiable_on E (FDIFF_1:def 6), 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
(a) is FDIFF_1:13/18 or POLYDIFF:14.
(b) is FDIFF_1:16/21 or POLYDIFF:16.
(c) is FDIFF_2:14/21.
for constant is FDIFF_1:11/22, see also POLYDIFF:11.
is FDIFF_1:17, see also POLYDIFF:12, and more general 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.
(a) is FDIFF_5:7.
(b) is FDIFF_5:17, although has been explicitly excluded, no reference for that.
Mean Value Theorems edit
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.
(a) is ROLLE:11 or FDIFF_2:31.
(b) is ROLLE:7.
(c) is ROLLE:12 or FDIFF_2:32.
The Continuity of Derivatives edit
5.12 Theorem No reference. #TODO implies the existence of an such that .
Corollary No reference.
L'Hospital's Rule edit
5.13 Theorem in L_HOSPIT, especially L_HOSPIT:10.
Derivatives of Higher Order edit
is diff(f,E).n (TAYLOR_1:def 5, see also TAYLOR_1:def 6), where is the domain on which is defined.
Taylor's Theorem edit
Set and , then is Partial_Sums(Taylor(f,E,c,d)).(n-'1) (see SERIES_1:def 1 and TAYLOR_1:def 7), where is the domain on which is defined. The theorem is TAYLOR_1:27 with instead of .
Differentiation of vector-valued Functions edit
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 and are given by CFDIFF_1:23/28, CFDIFF_1:26/31 respectively. No reference for .
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.
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.
is given by NDIFF_3:14/17. No reference for inner product.
5.17 Examples No reference. is defined in SIN_COS:def 14, is given by SIN_COS:25.
5.18 Examples No reference.
5.19 Theorem No reference.
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 implies .
27. No reference. #TODO Find reference for initial value problem.
28. No reference. #TODO Find reference for initial value problem.
29. No reference.