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

## Taylor's Theorem

5.15 Theorem
Set ${\displaystyle c=\alpha }$ and ${\displaystyle d=\beta }$, then ${\displaystyle P(t)}$ is Partial_Sums(Taylor(f,E,c,d)).(n-'1) (see SERIES_1:def 1 and TAYLOR_1:def 7), where ${\displaystyle E}$ is the domain on which ${\displaystyle f^{(n)}}$ is defined. The theorem is TAYLOR_1:27 with ${\displaystyle n+1}$ instead of ${\displaystyle 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 ${\displaystyle f+g}$ and ${\displaystyle fg}$ are given by CFDIFF_1:23/28, CFDIFF_1:26/31 respectively. No reference for ${\displaystyle 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.
${\displaystyle 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.
${\displaystyle f+g}$ is given by NDIFF_3:14/17. No reference for inner product.

5.17 Examples No reference. ${\displaystyle e^{z}}$ is defined in SIN_COS:def 14, ${\displaystyle 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 ${\displaystyle |f(x)|\leq A|f'(x)|}$ implies ${\displaystyle 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.