Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Numerical Sequences and Series

Convergent Sequences

3.1 Definition
A sequence $S$ of metric space $X$ is a sequence of X (STRUCT_0). $S$ can be convergent (TBSP_1:def 2) and $S$ converges to $x$ means S is_convergent_in_metrspace_to x (METRIC_6:def 2), in which case we may also write lim S = x (TBSP_1:def 3, METRIC_6:12). The range of any relation $R$ is initially defined in XTUPLE_0:def 13 and the synonym rng R is given in RELAT_1. $S$ is bounded (METRIC_6:def 4) if its range is bounded (TBSP_1:def 7, METRIC_6:def 3).

3.1 Definition (for complex and real numbers)
Complex_Sequence is defined in COMSEQ_1, Real_Sequence in SEQ_1. Convergence is COMSEQ_2:def 5 and SEQ_2:def 6, boundedness is COMSEQ_2:def 3/4. Limes is COMSEQ_2:def 6 for complex and SEQ_2:def 7 for real numbers. No reference for examples.

3.1 Definition (for real vectors)
Real_Sequence of N is defined in TOPRNS_1. Convergence is TOPRNS_1:def 8, boundedness is TOPRNS_1:def 7. Limes is TOPRNS_1:def 9.

3.2 Theorem
(a) No reference.
(b) Given by the uniqueness property of the different limes definitions.
(c) No reference for metric spaces. Clustered in COMSEQ_2 for complex and real sequences. Given for real vector sequences by TOPRNS_1:44.
(d) No reference.

3.3 Theorem
(a) is COMSEQ_2:14 and SEQ_2:6 (operation defined in VALUED_1:def 1).
(b) multiplication is COMSEQ_2:18 and SEQ_2:8 (operation defined in VALUED_1:def 5), no reference for addition (operation defined in VALUED_1:def 2).
(c) is COMSEQ_2:30 and SEQ_2:15 (operation defined in VALUED_1:def 4).
(d) is COMSEQ_2:35 and SEQ_2:22 (operation defined in VALUED_1:def 7).

3.4 Theorem
(a) No reference. #TODO Find reference that $x$ is convergent if each $x_{k}$ is convergent
(b) first one is TOPRNS_1:36, no reference for the other two.

Subsequences

3.5 Definition
subsequence is defined in VALUED_0:def 17. The first direction of the remark is given by METRIC_6:24 for metric spaces, SEQ_4:16 for real sequences, no reference for complex sequences, real vector sequences. The other direction has no reference.

3.6 Theorem
No reference for metric spaces or real vector sequences; COMSEQ_3:50 for complex and SEQ_4:40 for real sequences.

3.7 Theorem No reference.

Cauchy Sequences

3.8 Definition
TBSP_1:def 4 for metric spaces, no reference else.

3.9 Definition
TBSP_1:def 8 for subsets of metric spaces, MEASURE5:def 6 for sets of (extended) real numbers, no reference else. No reference for the remark.

3.10 Theorem No references.

3.11 Theorem
(a) TBSP_1:5 for metric spaces, implied by SEQ_4:41 for real sequences, no references else. (b) TBSP_1:8 in combination with TBSP_1:def 5 for metric spaces, again implied by SEQ_4:41 for real sequences, no references else. (c) No reference.

3.12 Definition is TBSP_1:def 5. No reference for remark.

3.13 Definition
Monotonically increasing is non-decreasing (SEQM_3:def 8), monotonically decreasing is non-increasing (SEQM_3:def 9). Monotonic is monotone (SEQM_3:def 5).

3.14 Theorem is SEQ_2:13 and SEQ_4:36 (both clustered in the respective article).

Upper And Lower Limits

3.15 Definition
$s_{n}\rightarrow +\infty$ means s is non bounded_above (SEQ_2:def 1). $s_{n}\rightarrow -\infty$ means s is non bounded_below (SEQ_2:def 2). For extended real sequences (defined in MESFUNC5) the variants convergent_to_+/-infty (MESFUNC5:def 9/10) exist.

3.16 Definition
The definition in the Book has no reference. However, lim_sup/inf are defined in RINFSUP1:def 6/7 and RINFSUP2:def 8/9 respectively. The first variant maps real sequences to reals, therefore excluding $\pm \infty$, the second one maps extended real sequences to extended reals, thereby allowing $\pm \infty$. The identification of the variants for bounded sequences is given by RINFSUP2:9/10.

3.17 Theorem
(a) No reference, except maybe in the case of $\pm \infty$ where it holds by definition.
(b) Implicitly given by RINFSUP1:82/84.
The uniquess property are given again in the definition of the functors.

3.18 Examples
(a) No reference.
(b) No reference.
(c) Given by RINFSUP1:88/89 or RINFSUP2:40/41.

3.19 Theorem
No direct reference, but can be followed from RINFSUP1:91 ($N=0$) in combination with RINFSUP2:28/29.

Some Special Sequences

Remark is SEQ_2:17 with SEQ_2:18, which is a weaker version of the sandwich lemma SEQ_2:19.

3.20 Theorem
(a) ASYMPT_1:69 is stronger version
(b) is PREPOWER:33 or POWER:23.
(c) No reference.
(d) No reference.
(e) is SERIES_1:3.

Series

3.21 Definition
The sum $\sum _{n=p}^{q}a_{n}$ for $p\leq q$ can be expressed via Sum(a, p, q) (SERIES_1:def 6) if $a$ is a sequence.
However, that notation is used rather seldom in the MML. The usual approach is to have the summands as a tuple (in form of a FinSequence (FINSEQ_1) of real or complex numbers) and use Sum a (RVSUM_1:def 10). The usual operations of sums are defined in RVSUM_1/2, too. If the upper and lower limit are indeed needed, a possible variant would be Sum (a|q/^p) (FINSEQ_1:def 15, RFINSEQ:def 1). Also see NEWTON04:37.
In comparison to that, $s_{n}$ is simply Partial_Sums(s) (SERIES_1:def 1). The series converging means a is summable (SERIES_1:def 2 for real, COMSEQ_3:def 8 for complex), it limes is Sum a (SERIES_1:def 3). (Note that in the paragraph above, a referred to a FinSequence, while in this paragraph, it refers to a Real_sequence, so the Sum functors with a single argument behind it in these both paragraphs are different ones.)
Note that series in Mizar always start with $0$ because they are ManySortedSet of NAT and 0 in NAT. Inconvenient summands, like ${\tfrac {1}{0}}$ in the series of ${\tfrac {1}{n}}$, usually turn out to be 0 in Mizar, or the sequence to be summed is defined to be fitting with this notation just beforehand.

3.22 Theorem is SERIES_1:21.

3.23 Theorem is SERIES_1:4.

3.24 Theorem is SERIES_1:17.

3.25 Theorem
(a) COMSEQ_3:66, weaker version is SERIES_1:19.
(b) No reference.

Series Of Nonnegative Terms

3.26 Theorem
The geometric sequence is defined in PREPOWER:def 1 for real base and in COMSEQ_3:def 1 for complex base. Their sum for $|x|<1$ is given by SERIES_1:24 or COMSEQ_3:64 for $x$ being real or complex respectively. No reference for $|x|\geq 1$.

3.27 Theorem is SERIES_1:31 or COMSEQ_3:72 for real or complex sequences respectively.

3.28 Theorem is SERIES_1:32/33 or COMSEQ_3:73/74 for real or complex sequences respectively.

3.29 Theorem No reference.

The Number $e$

3.30 Definition
$n!$ is defined in NEWTON:def 2. $e$ is number_e (POWER:def 4), $e^{x}$ is exp_R (SIN_COS:def 22). $e=e^{1}$ is given by IRRAT_1:def 7. Then the definition of the Book is given by IRRAT_1:def 5 and IRRAT_1:23.

3.31 Theorem is given by IRRAT_1:def 4 and IRRAT_1:22.

3.32 Theorem is IRRAT_1:41.

The Root And Ratio Tests

3.33 Theorem
(a) is basically SERIES_1:40 or COMSEQ_3:69 for real or complex sequences respectively.
(b) is basically SERIES_1:41 or COMSEQ_3:70 for real or complex sequences respectively.
(c) No reference.

3.34 Theorem
(a) is basically SERIES_1:37 or COMSEQ_3:75 for real or complex sequences respectively.
(a) is basically SERIES_1:39 or COMSEQ_3:76 for real or complex sequences respectively.

3.35 Examples No reference.

3.36 Remark Nothing to formalize.

3.37 Theorem No reference.

Power Series

3.38 Definition No reference.

3.39 Theorem No reference.

3.40 Examples No reference.

Summation By Parts

3.41 Theorem No reference.

3.42 Theorem No reference.

3.43 Theorem is LEIBNIZ1:8.

3.44 Theorem No reference.

Absolute Convergence

$a$ converging absolutely means a is absolutely_summable (SERIES_1:def 4 or COMSEQ_3:def 9).

3.45 Theorem is SERIES_1:35 or COMSEQ_3:63 and clustered in both articles.

3.46 Remark No reference.

Addition And Multiplication Of Series

3.47 Theorem
For real sequences, SERIES_1:7 and SERIES_1:10.
For complex sequences, COMSEQ_3:54 and COMSEQ_3:56.

3.48 Definition No reference. #TODO Find reference for Cauchy product of two series.

3.49 Example No reference.

3.50 Theorem No reference.

3.51 Theorem No reference.

Rearrangements

3.52 Definition
A Permutation of NAT is defined in FUNCT_2, but no reference for rearrangements.

3.53 Example No reference.

3.54 Theorem No reference.

3.55 Theorem No reference.

Exercises

1. clustered in SEQ_2 for real sequences, no reference for complex sequences or converse (which is false).
2. No reference.
3. No reference.
4. No reference.
5. is in RINFSUP1:92 in bounded case, for the other one 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. #TODO Find reference that Cauchy product of two abs conv series is abs conv.
14. No reference.
15. No reference.
16. No reference. #TODO Find reference for convergence towards ${\sqrt {\alpha }}$
17. No reference.
18. No reference.
19. No reference. #TODO Find reference for ternary representation of reals in the Cantor set.
20. No reference.
21. No reference.
22. No reference. #TODO Find reference for Baire's theorem
23. No reference.
24. No reference.
25. No reference.