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 $\varphi (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^{\prime }(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^{\prime }$ 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^{\prime }=0$ for constant $c$ is FDIFF_1:11/22, see also POLYDIFF:11.
$x^{\prime }=1$ is FDIFF_1:17, see also POLYDIFF:12, and more general $(ax+b{)}^{\prime }=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^{\prime }(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^{\prime }(a)<\lambda <f^{\prime }(b)$ implies the existence of an $x$ such that $f^{\prime }(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)|\le A|f^{\prime }(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.