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

Power Series

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

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. $e^{0}=1$ 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).

$E(L(y))=y$ is given by POWER:def 3 or TAYLOR_1:14/15, $L(E(x))=x$ is given by TAYLOR_1:12/13 or MOEBIUS3:16. $L'(y)={\tfrac {1}{y}}$ 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. $x^{\alpha }=e^{\alpha \log x}$ is given by FDIFF_6:1. No reference for $\log x$ being lower than any positive power of $x$.

The Trigonometric Functions

$C(x)$ and $S(x)$ are defined in SIN_COS3:def 2 and SIN_COS3:def 1 respectively. $E(ix)=C(x)+iS(x)$ is given by SIN_COS3:36 (or more general by SIN_COS3:19). $|E(ix)|=1$ is given by SIN_COS:27. No reference for derivates in complex case, but in real case given by SIN_COS:63/64. $\pi$ in Mizar is defined as the unique $x\in (0,4)$ such that $\tan {\tfrac {\pi }{4}}=1$ (SIN_COS:def 28). $\cos(2\pi )=0$ is given by SIN_COS:76/77, that $\pi$ 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

8.8 Theorem is POLYNOM5:74.

Fourier Series

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

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

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 $x=1$ 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.