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. 沒有引用。