Walter Rudin 的《数学分析原理》Mizar 注解/一些特殊函数

幂级数

8.1 定理 无参考。

推论 无参考。

8.2 定理 无参考。

8.3 定理 无参考，但参见DBLSEQ_1/2.

8.4 定理 无参考。

8.5 定理 无参考。

指数函数和对数函数

指数函数的级数展开由以下给出SIN_COS:def 5以及TAYLOR_2:16.

8.6 定理
(a) 连续性集中在SIN_COS中，可微性由以下给出TAYLOR_1:16.
(b)TAYLOR_1:16, SIN_COS:65/66或INTEGRA8:32.
(c) 单调性隐含地由以下给出，正性也隐含地存在，但也由以下显式给出TAYLOR_1:16,SIN_COS:52/53.
(d)SIN_COS:23或SIN_COS:46. SIN_COS:50或SIN_COS2:12仅对实数。 $e^{0}=1$ 由以下给出SIN_COS:51或SIN_COS2:13.
(e) 没有直接的参考极限，但参见TAYLOR_1:16，其中它们是隐式给出的。
(f) 隐含地由以下给出ASYMPT_2:25(结合ASYMPT_0:15-17以及ASYMPT_2:def 1).

$E(L(y))=y$ 由以下给出POWER:def 3或TAYLOR_1:14/15，$L(E(x))=x$ 由以下给出TAYLOR_1:12/13或MOEBIUS3:16。 $L'(y)={\tfrac {1}{y}}$ 由以下给出FDIFF_4:1或TAYLOR_1:18。对数的加法公式由以下给出POWER:53或MOEBIUS3:19。极限再次仅由以下间接给出TAYLOR_1:18。 $x^{\alpha }=e^{\alpha \log x}$ 由以下给出FDIFF_6:1。无关于 $\log x$ 小于 $x$ 的任何正幂的参考。

三角函数

$C(x)$ 和 $S(x)$ 分别在以下定义SIN_COS3:def 2以及SIN_COS3:def 1。 $E(ix)=C(x)+iS(x)$ 由以下给出SIN_COS3:36(或更一般地由以下给出SIN_COS3:19)。 $|E(ix)|=1$ 由以下给出SIN_COS:27。在复数情况下没有导数的参考，但在实数情况下由以下给出SIN_COS:63/64。在 Mizar 中，$\pi$ 定义为唯一的 $x\in (0,4)$，使得 $\tan {\tfrac {\pi }{4}}=1$（SIN_COS:def 28

). $\cos(2\pi )=0$ 由以下给出SIN_COS:76/77, 即 $\pi$ 是具有该性质的最小正数，由以下给出SIN_COS:80/81. 其余性质由以下给出SIN_COS3:27-33.

8.7 定理
(a) 没有直接引用，仅隐含地由以下给出SIN_COS3:27.
(b)SIN_COS3:35/34(复数) 或SIN_COS2:11/10(实数).
(c) 没有引用。
(d) 没有引用。

单位圆的周长没有引用，但请参见TOPREALB:def 11了解其参数化。

复数域的代数完备性

8.8 定理 为POLYNOM5:74.

傅里叶级数

8.9 定义 没有引用。

8.10 定义 没有引用。

8.11 定理 没有引用。

8.12 定理 没有引用。

8.13 三角级数 没有引用。

8.14 定理 没有引用。

推论 无参考。

8.15 定理 没有引用。

8.16 定理 没有引用。

伽马函数

8.17 定义 没有引用。

8.18 定理 没有引用。

8.19 定理 没有引用。

8.20 定理 没有引用。

8.21 一些推论 没有引用。

8.22 斯特林公式 没有引用。

练习

1. 没有引用。
2. 没有引用。
3. 没有引用。
4.(a) 没有引用。
4.(b) 没有引用。
4.(c) 没有引用。
4.(d) 没有引用，除了 $x=1$ 在IRRAT_1:22(参见IRRAT_1:def 4).
5. 没有引用。
6. 没有引用。
7. 没有引用。
8. 没有引用。
9. 没有引用。
10. 没有引用。
11. 没有引用。
12. 没有引用。
13. 没有引用，但结果为BASEL_2:32(另见BASEL_1:31).
14. 没有引用。
15. 没有引用。
16. 没有引用。
17. 没有引用。
18. 没有引用。
19. 没有引用。
20. 没有引用。
21. 没有引用。
22. 没有引用。
23. 没有引用。
24. 没有引用。
25. 没有引用。
26. 没有引用。
27. 没有引用。
28. 没有引用。
29. 为BROUWER:15.
30. 没有引用。
31. 没有引用。