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

## The Derivative of a Real Function

edit**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 Theorems

edit**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

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

**Corollary** No reference.

## L'Hospital's Rule

edit**5.13 Theorem** in `L_HOSPIT`, especially `L_HOSPIT:10`.

## Derivatives of Higher Order

edit**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 Theorem

edit**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 Functions

edit**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.

## Exercises

edit1. 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.