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. 参考文献缺失。