# 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 <f'(b)$ 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

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