# 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 $\phi (t)$  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 $[a,b]$ .)
$f$  is differentiable at $x$  means f is_differentiable_in x (FDIFF_1:def 4), $f'(x)$  is diff(f,x) (FDIFF_1:def 5). $f$  is differentiable on $E$  means f is_differentiable_on E (FDIFF_1:def 6), $f'$  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
$c'=0$  for constant $c$  is FDIFF_1:11/22, see also POLYDIFF:11.
$x'=1$  is FDIFF_1:17, see also POLYDIFF:12, and more general $(ax+b)'=a$  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 $f'(0)$  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 $f'(a)<\lambda   implies the existence of an $x$  such that $f'(x)=\lambda$ .

Corollary No reference.

## L'Hospital's Rule

5.13 Theorem in L_HOSPIT, especially L_HOSPIT:10.

## Derivatives of Higher Order

5.14 Definition
$f^{(n)}$  is diff(f,E).n (TAYLOR_1:def 5, see also TAYLOR_1:def 6), where $E$  is the domain on which $f^{(n)}$  is defined.

## Taylor's Theorem

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

## Differentiation of vector-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 $f+g$  and $fg$  are given by CFDIFF_1:23/28, CFDIFF_1:26/31 respectively. No reference for $f/g$ .

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.
$f+g$  is given by NDIFF_1:35/39. No reference for inner product.

That differentiability implies continuity is given by NDIFF_3:22/23.
$f+g$  is given by NDIFF_3:14/17. No reference for inner product.

5.17 Examples No reference. $e^{z}$  is defined in SIN_COS:def 14, $e^{ix}$  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 $|f(x)|\leq A|f'(x)|$  implies $f=0$ .
27. No reference. #TODO Find reference for initial value problem.
28. No reference. #TODO Find reference for initial value problem.
29. No reference.