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

From Wikibooks, open books for an open world
Jump to navigation Jump to search

The Derivative of a Real Function[edit]

5.1 Definition
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

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

5.6 Examples
(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.

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

5.14 Definition
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]

5.15 Theorem
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.

Exercises[edit]

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.