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

The Derivative of a Real FunctionEdit

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 TheoremsEdit

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 DerivativesEdit

5.12 Theorem No reference. #TODO   implies the existence of an   such that  .

Corollary No reference.

L'Hospital's RuleEdit

5.13 Theorem in L_HOSPIT, especially L_HOSPIT:10.

Derivatives of Higher OrderEdit

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 TheoremEdit

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 FunctionsEdit

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.

ExercisesEdit

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.