Mizar 對 Walter Rudin 的 《數學分析原理》/數值序列和級數的評註

收斂序列

3.1 定義
度量空間 $X$ 中的序列 $S$ 是X 的序列 (STRUCT_0）。$S$ 可以收斂 (TBSP_1:def 2)，並且 $S$ 收斂於 $x$ 意味著S 在度量空間中收斂於 x (METRIC_6:def 2)，在這種情況下我們也可以寫成lim S = x (TBSP_1:def 3, METRIC_6:12)。任何關係 $R$ 的值域最初是在XTUPLE_0:def 13中定義的，並且同義詞rng R在RELAT_1中給出。 $S$ 是有界的 (METRIC_6:def 4)，如果它的值域是有界的（TBSP_1:def 7, METRIC_6:def 3).

3.1 定義（對於複數和實數）
復序列在COMSEQ_1, 中定義，實序列在SEQ_1中定義。收斂性是COMSEQ_2:def 5和SEQ_2:def 6，有界性是COMSEQ_2:def 3/4。極限是COMSEQ_2:def 6對於複數，以及SEQ_2:def 7

對於實數。沒有參考的例子。
3.1 定義（對於實向量）在N 的實序列SEQ_1TOPRNS_1SEQ_2:def 6TOPRNS_1:def 8COMSEQ_2:def 3/4TOPRNS_1:def 7.

TOPRNS_1:def 9
3.2 定理
(a) 沒有參考。(b) 由不同極限定義的唯一性
性質給出。(c) 度量空間沒有參考。在COMSEQ_2中對於復序列和實序列進行聚類。由.
TOPRNS_1:44

給出，用於實向量序列。
(d) 沒有參考。3.3 定理COMSEQ_2:def 5(a) 是COMSEQ_2:14SEQ_2:6).
（操作定義在VALUED_1:def 1COMSEQ_2:def 5中）。COMSEQ_2:14(b) 乘法是COMSEQ_2:18SEQ_2:8).
VALUED_1:def 5)，加法沒有參考（操作定義在COMSEQ_2:def 5VALUED_1:def 2COMSEQ_2:14中）。).
(c) 是COMSEQ_2:30COMSEQ_2:def 5SEQ_2:15COMSEQ_2:14VALUED_1:def 4).

。
(d) 是
COMSEQ_2:35SEQ_2:22VALUED_1:def 7

。

(a) 沒有參考。#TODO 找到 $x$ 是收斂的，如果每個 $x_{k}$ 是收斂的參考。
(b) 第一個是在TOPRNS_1:36，另外兩個沒有參考。子序列[編輯 | 編輯原始碼]3.5 定義子序列

VALUED_0:def 17
。該註解的第一方向由METRIC_6:24COMSEQ_2:def 6給出，用於度量空間，SEQ_4:16

給出，用於實數序列，復序列和實向量序列沒有參考。另一個方向沒有參考。

3.6 定理

COMSEQ_3:50
SEQ_4:40給出，用於實數序列。

**3.7 定理** 沒有參考。
柯西序列[編輯 | 編輯原始碼]3.8 定義TBSP_1:def 4

給出，用於度量空間，其他沒有參考。

3.9 定義
TBSP_1:def 8給出，用於度量空間的子集，MEASURE5:def 6給出，用於（擴充套件）實數集，其他沒有參考。該註解沒有參考。**3.10 定理** 沒有參考。3.11 定理(a)TBSP_1:5給出，用於度量空間，由給出，用於（擴充套件）實數集，其他沒有參考。該註解沒有參考。SEQ_4:41

給出，用於實數序列，其他沒有參考。 (b)TBSP_1:5TBSP_1:8

與
TBSP_1:def 5結合給出，用於度量空間，再次由 (給出，用於實數序列，其他沒有參考。(c) 沒有參考。**3.12 定義** 是。該註解沒有參考。 (3.13 定義單調遞增是非遞減 (SEQM_3:def 8).

)，單調遞減是非遞增COMSEQ_2:def 5SEQM_3:def 9)。單調是

單調的

**3.14 定理** 是
SEQ_2:13SEQ_4:36 (（兩者都聚類在各自的文章中）。). $s_{n}\rightarrow -\infty$ 表示s 是無下界的 (SEQ_2:def 2). 對於擴充套件實數序列（定義在MESFUNC5）中，存在以下變體收斂到+/-無窮 (MESFUNC5:def 9/10）。

3.16 定義
書中的定義沒有引用。然而，lim_sup/inf定義在RINFSUP1:def 6/7COMSEQ_2:def 5RINFSUP2:def 8/9中，分別。第一個變體將實數序列對映到實數，因此排除了 $\pm \infty$，第二個變體將擴充套件實數序列對映到擴充套件實數，從而允許 $\pm \infty$。有界序列的變體標識由以下給出RINFSUP2:9/10.

3.17 定理
(a) 沒有引用，除了可能在 $\pm \infty$ 的情況下，它根據定義成立。
(b) 由以下隱式給出RINFSUP1:82/84.
唯一性屬性再次在函子的定義中給出。

3.18 例子
3.2 定理
(b) 沒有引用。
(c) 由以下給出RINFSUP1:88/89或RINFSUP2:40/41.

3.19 定理
沒有直接引用，但可以從以下推斷出來RINFSUP1:91($N=0$) 與RINFSUP2:28/29.

一些特殊序列

備註是SEQ_2:17與SEQ_2:18，這是夾逼定理的較弱版本SEQ_2:19.

3.20 定理
TBSP_1:def 8ASYMPT_1:69是較強版本
(b) 是PREPOWER:33或POWER:23.
(c) 沒有引用。
TOPRNS_1:44
(e) 是SERIES_1:3.

級數

3.21 定義
和 $\sum _{n=p}^{q}a_{n}$ 對於 $p\leq q$ 可以用以下方式表示Sum(a, p, q) (SERIES_1:def 6）如果 $a$ 是一個序列。
然而，這種表示方法在 MML 中很少使用。通常的做法是將被加數作為一個元組（以FinSequence (FINSEQ_1）的形式，它包含實數或複數），並使用Sum a (RVSUM_1:def 10）。和的常用運算定義在RVSUM_1/2中。如果確實需要上限和下限，一個可能的變體是Sum (a|q/^p) (FINSEQ_1:def 15, RFINSEQ:def 1）。另請參閱NEWTON04:37.
與之相比，$s_{n}$ 僅僅是Partial_Sums(s) (SERIES_1:def 1）。級數收斂意味著a 是可求和的 (SERIES_1:def 2對於實數，COMSEQ_3:def 8對於複數），它的極限是Sum a (SERIES_1:def 3）。（注意，在上面的段落中，a指的是一個FinSequence，而在本段落中，它指的是一個Real_sequence，因此在這兩個段落中，帶有單個引數的Sum函子是不同的。)
注意，在 Mizar 中，級數總是從 $0$ 開始，因為它們是ManySortedSet of NATCOMSEQ_2:def 50 in NAT。不方便的被加數，例如 ${\tfrac {1}{0}}$ 在 ${\tfrac {1}{n}}$ 的級數中，通常會變成0在 Mizar 中，或者求和的序列被定義為事先適合這種表示法。

3.22 定理 是SERIES_1:21.

3.23 定理 是SERIES_1:4.

3.24 定理 是SERIES_1:17.

3.25 定理
TBSP_1:def 8COMSEQ_3:66，較弱版本為SERIES_1:19.
(b) 沒有引用。

非負項級數

3.26 定理
幾何級數定義在PREPOWER:def 1對於實數底，以及在COMSEQ_3:def 1對於複數底。它們對於 $|x|<1$ 的和由SERIES_1:24或COMSEQ_3:64對於 $x$ 分別為實數或複數給出。對於 $|x|\geq 1$ 沒有參考。

3.27 定理 是SERIES_1:31或COMSEQ_3:72分別對於實數或複數序列。

3.28 定理 是SERIES_1:32/33或COMSEQ_3:73/74分別對於實數或複數序列。

3.29 定理 沒有參考。

數 $e$

3.30 定義
$n!$ 定義在NEWTON:def 2. $e$ 是number_e (POWER:def 4), $e^{x}$ 是exp_R (SIN_COS:def 22). $e=e^{1}$ 由IRRAT_1:def 7給出。那麼書中的定義由IRRAT_1:def 5COMSEQ_2:def 5IRRAT_1:23.

3.31 定理 由IRRAT_1:def 4COMSEQ_2:def 5IRRAT_1:22.

3.32 定理 是IRRAT_1:41.

根式檢驗和比式檢驗

3.33 定理
(a) 基本上是SERIES_1:40或COMSEQ_3:69分別對於實數或複數序列。
(b) 基本上是SERIES_1:41或COMSEQ_3:70分別對於實數或複數序列。
(c) 沒有引用。

3.34 定理
(a) 基本上是SERIES_1:37或COMSEQ_3:75分別對於實數或複數序列。
(a) 基本上是SERIES_1:39或COMSEQ_3:76分別對於實數或複數序列。

3.35 例子 沒有參考。

3.36 備註 沒有需要形式化的內容。

3.37 定理 沒有參考。

冪級數

3.38 定義 沒有參考。

3.39 定理 沒有參考。

3.40 例子 沒有參考。

分部求和

3.41 定理 沒有參考。

3.42 定理 沒有參考。

3.43 定理 是LEIBNIZ1:8.

3.44 定理 沒有參考。

絕對收斂

$a$ 絕對收斂意味著a 是 absolutely_summable (SERIES_1:def 4或COMSEQ_3:def 9).

3.45 定理 是SERIES_1:35或COMSEQ_3:63並且在這兩篇文章中都集中在一起。

3.46 備註 沒有參考。

級數的加法和乘法

3.47 定理
對於實數序列，SERIES_1:7COMSEQ_2:def 5SERIES_1:10.
對於複數序列，COMSEQ_3:54COMSEQ_2:def 5COMSEQ_3:56.

3.48 定義 沒有參考。#TODO 找到兩個級數的柯西乘積的參考。

3.49 例子 沒有參考。

3.50 定理 沒有參考。

3.51 定理 沒有參考。

重排

3.52 定義
一個NAT 的排列在FUNCT_2，但沒有關於重排的參考。

3.53 例子 沒有參考。

3.54 定理 沒有參考。

3.55 定理 沒有參考。

習題

1. 集中在SEQ_2對於實數序列，沒有關於複數序列或逆命題（它是錯誤的）的參考。
2. 沒有參考。
3. 沒有參考。
4. 沒有參考。
5. 在RINFSUP1:92有界情況下，對於另一個沒有參考。
6. 沒有參考。
7. 沒有參考。
8. 沒有參考。
9. 沒有參考。
10. 沒有參考。
11. 沒有參考。
12. 沒有參考。
13. 沒有參考。#TODO 找到兩個絕對收斂級數的柯西乘積也是絕對收斂的參考。
14. 沒有參考。
15. 沒有參考。
16. 參考文獻缺失。#TODO 找到關於收斂於 ${\sqrt {\alpha }}$ 的參考資料。
17. 參考文獻缺失。
18. 參考文獻缺失。
19. 參考文獻缺失。#TODO 找到關於康托爾集上實數的三進製表示的參考資料。
20. 參考文獻缺失。
21. 參考文獻缺失。
22. 參考文獻缺失。#TODO 找到關於貝爾定理的參考資料。
23. 參考文獻缺失。
24. 參考文獻缺失。
25. 參考文獻缺失。