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

## Convergent SequencesEdit

**3.1 Definition**

A sequence of metric space is a `sequence of X` (`STRUCT_0`). can be `convergent` (`TBSP_1:def 2`) and converges to 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 is initially defined in `XTUPLE_0:def 13` and the synonym `rng R` is given in `RELAT_1`. 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 is convergent if each is convergent

(b) first one is `TOPRNS_1:36`, no reference for the other two.

## SubsequencesEdit

**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 SequencesEdit

**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 LimitsEdit

**3.15 Definition**

means `s is non bounded_above` (`SEQ_2:def 1`). 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 , the second one maps extended real sequences to extended reals, thereby allowing . 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 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` ( ) in combination with `RINFSUP2:28/29`.

## Some Special SequencesEdit

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`.

## SeriesEdit

**3.21 Definition**

The sum for can be expressed via `Sum(a, p, q)` (`SERIES_1:def 6`) if 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, 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 because they are `ManySortedSet of NAT` and `0 in NAT`. Inconvenient summands, like in the series of , 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 TermsEdit

**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 is given by `SERIES_1:24` or `COMSEQ_3:64` for being real or complex respectively. No reference for .

**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 Edit

**3.30 Definition**

is defined in `NEWTON:def 2`. is `number_e` (`POWER:def 4`), is `exp_R` (`SIN_COS:def 22`). 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 TestsEdit

**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 SeriesEdit

**3.38 Definition** No reference.

**3.39 Theorem** No reference.

**3.40 Examples** No reference.

## Summation By PartsEdit

**3.41 Theorem** No reference.

**3.42 Theorem** No reference.

**3.43 Theorem** is `LEIBNIZ1:8`.

**3.44 Theorem** No reference.

## Absolute ConvergenceEdit

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 SeriesEdit

**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.

## RearrangementsEdit

**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.

## ExercisesEdit

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

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.