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

Convergent Sequences 3.1 Definition A sequence of metric space is a (). can be () and converges to means (), in which case we may also write (, ). The range of any relation is initially defined in and the synonym is given in . is () if its range is bounded (, ). 3.1 Definition (for complex and real numbers) is defined in , in . Convergence is and , boundedness is . Limes is for complex and for real numbers. No reference for examples. 3.1 Definition (for real vectors) is defined in . Convergence is , boundedness is . Limes is . 3.2 Theorem (a) No reference. (b) Given by the property of the different limes definitions. (c) No reference for metric spaces. Clustered in for complex and real sequences. Given for real vector sequences by . (d) No reference. 3.3 Theorem (a) is and (operation defined in ). (b) multiplication is and (operation defined in ), no reference for addition (operation defined in ). (c) is and (operation defined in ). (d) is and (operation defined in ). 3.4 Theorem (a) No reference. #TODO Find reference that is convergent if each is convergent (b) first one is , no reference for the other two. Subsequences 3.5 Definition is defined in . The first direction of the remark is given by for metric spaces, 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; for complex and for real sequences. 3.7 Theorem No reference. Cauchy Sequences 3.8 Definition for metric spaces, no reference else. 3.9 Definition for subsets of metric spaces, for sets of (extended) real numbers, no reference else. No reference for the remark. 3.10 Theorem No references. 3.11 Theorem (a) for metric spaces, implied by for real sequences, no references else. (b) in combination with for metric spaces, again implied by for real sequences, no references else. (c) No reference. 3.12 Definition is . No reference for remark. 3.13 Definition Monotonically increasing is (), monotonically decreasing is (). Monotonic is (). 3.14 Theorem is and (both clustered in the respective article). Upper And Lower Limits 3.15 Definition means (). means (). For extended real sequences (defined in ) the variants () exist. 3.16 Definition The definition in the Book has no reference. However, are defined in and 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 . 3.17 Theorem (a) No reference, except maybe in the case of where it holds by definition. (b) Implicitly given by . The uniquess property are given again in the definition of the functors. 3.18 Examples (a) No reference. (b) No reference. (c) Given by or . 3.19 Theorem No direct reference, but can be followed from () in combination with . Some Special Sequences Remark is with , which is a weaker version of the sandwich lemma . 3.20 Theorem (a) is stronger version (b) is or . (c) No reference. (d) No reference. (e) is . Series 3.21 Definition The sum for can be expressed via () 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 () of real or complex numbers) and use (). The usual operations of sums are defined in , too. If the upper and lower limit are indeed needed, a possible variant would be (, ). Also see . In comparison to that, is simply (). The series converging means ( for real, for complex), it limes is (). (Note that in the paragraph above, referred to a , while in this paragraph, it refers to a , so the 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 and . Inconvenient summands, like in the series of , usually turn out to be in Mizar, or the sequence to be summed is defined to be fitting with this notation just beforehand. 3.22 Theorem is . 3.23 Theorem is . 3.24 Theorem is . 3.25 Theorem (a) , weaker version is . (b) No reference. Series Of Nonnegative Terms 3.26 Theorem The geometric sequence is defined in for real base and in for complex base. Their sum for is given by or for being real or complex respectively. No reference for . 3.27 Theorem is or for real or complex sequences respectively. 3.28 Theorem is or for real or complex sequences respectively. 3.29 Theorem No reference. The Number 3.30 Definition is defined in . is (), is (). is given by . Then the definition of the Book is given by and . 3.31 Theorem is given by and . 3.32 Theorem is . The Root And Ratio Tests 3.33 Theorem (a) is basically or for real or complex sequences respectively. (b) is basically or for real or complex sequences respectively. (c) No reference. 3.34 Theorem (a) is basically or for real or complex sequences respectively. (a) is basically or 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 . 3.44 Theorem No reference. Absolute Convergence converging absolutely means ( or ). 3.45 Theorem is or and clustered in both articles. 3.46 Remark No reference. Addition And Multiplication Of Series 3.47 Theorem For real sequences, and . For complex sequences, and . 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 is defined in , but no reference for rearrangements. 3.53 Example No reference. 3.54 Theorem No reference. 3.55 Theorem No reference. Exercises 1. clustered in 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 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.