# Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Some Special Functions

## Power Series[edit | edit source]

**8.1 Theorem** No reference.

**Corollary** No reference.

**8.2 Theorem** No reference.

**8.3 Theorem** No reference, but see `DBLSEQ_1/2`.

**8.4 Theorem** No reference.

**8.5 Theorem** No reference.

## The Exponential and Logarithmic Functions[edit | edit source]

The series expansion of the exponential function is given via `SIN_COS:def 5` and `TAYLOR_2:16`.

**8.6 Theorem**

(a) Continuity is clustered in `SIN_COS`, differentiability is given by `TAYLOR_1:16`.

(b) `TAYLOR_1:16`, `SIN_COS:65/66` or `INTEGRA8:32`.

(c) Monotonicity implicitly given by `TAYLOR_1:16`, positivity implicitly there too, but also explicitly by `SIN_COS:52/53`.

(d) `SIN_COS:23` or `SIN_COS:46`. `SIN_COS:50` or `SIN_COS2:12` for reals only. is given by `SIN_COS:51` or `SIN_COS2:13`.

(e) No direct reference for the limits but see `TAYLOR_1:16`, where they are implicitly given.

(f) Implicitly given by `ASYMPT_2:25` (in combination with `ASYMPT_0:15-17` and `ASYMPT_2:def 1`).

is given by `POWER:def 3` or `TAYLOR_1:14/15`, is given by `TAYLOR_1:12/13` or `MOEBIUS3:16`. is given by `FDIFF_4:1` or `TAYLOR_1:18`. The addition formula for logarithms is given by `POWER:53` or `MOEBIUS3:19`. The limits are again only indirectly given by `TAYLOR_1:18`. is given by `FDIFF_6:1`. No reference for being lower than any positive power of .

## The Trigonometric Functions[edit | edit source]

and are defined in `SIN_COS3:def 2` and `SIN_COS3:def 1` respectively. is given by `SIN_COS3:36` (or more general by `SIN_COS3:19`). is given by `SIN_COS:27`. No reference for derivates in complex case, but in real case given by `SIN_COS:63/64`. in Mizar is defined as the unique such that (`SIN_COS:def 28`). is given by `SIN_COS:76/77`, that is the smallest positive number with that property is given by `SIN_COS:80/81`. The rest of the properties is given by `SIN_COS3:27-33`.

**8.7 Theorem**

(a) No direct reference, only implicitly by `SIN_COS3:27`.

(b) `SIN_COS3:35/34` (complex) or `SIN_COS2:11/10` (real).

(c) No reference.

(d) No reference.

No reference for the circumference of the unit circle, but see `TOPREALB:def 11` for a parametrization of it.

## The Algebraic Completeness of the Complex Field[edit | edit source]

**8.8 Theorem** is `POLYNOM5:74`.

## Fourier Series[edit | edit source]

**8.9 Definition** No reference.

**8.10 Definition** No reference.

**8.11 Theorem** No reference.

**8.12 Theorem** No reference.

**8.13 Trigonometric series** No reference.

**8.14 Theorem** No reference.

**Corollary** No reference.

**8.15 Theorem** No reference.

**8.16 Theorem** No reference.

## The Gamma Function[edit | edit source]

**8.17 Definition** No reference.

**8.18 Theorem** No reference.

**8.19 Theorem** No reference.

**8.20 Theorem** No reference.

**8.21 Some consequences** No reference.

**8.22 Stirling's formula** No reference.

## Exercises[edit | edit source]

1. No reference.

2. No reference.

3. No reference.

4.(a) No reference.

4.(b) No reference.

4.(c) No reference.

4.(d) No reference, except for in `IRRAT_1:22` (see `IRRAT_1:def 4`).

5. No reference.

6. No reference.

7. No reference.

8. No reference.

9. No reference.

10. No reference.

11. No reference.

12. No reference.

13. No reference, but the result is `BASEL_2:32` (see also `BASEL_1:31`).

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.

27. No reference.

28. No reference.

29. is `BROUWER:15`.

30. No reference.

31. No reference.