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

Note that sequences of functions can be seen as sequences over a normed space, which will mostly be left untouched in this chapter. Discussion of main problem 7.1 Definition Let denote . being pointwise convergent is described by F is_point_conv_on E (SEQFUNC:20, see also SEQFUNC:def 10). Then is given by lim(F,E) (SEQFUNC:def 13). No reference for series. 7.2 Example No reference. 7.3 Example No reference. 7.4 Example No reference. 7.5 Example No reference. 7.6 Example No reference. Uniform Convergence 7.7 Definition being uniformly convergent on is F is_unif_conv_on E (SEQFUNC:def 12) or F is_uniformly_convergent_to f (MESFUN10:def 2. That uniform convergence implies pointwise convergence is SEQFUNC:22 or MESFUN10:20. No reference for function series. 7.8 Theorem No reference. 7.9 Theorem No reference. 7.10 Theorem No reference. Uniform Convergence and Continuity 7.11 Theorem No direct reference, but implicitly given in proof of TIETZE:20. 7.12 Theorem is TIETZE:20. 7.13 Theorem No reference. 7.14 Definition No reference. 7.15 Theorem No reference. Uniform Convergence and Integration 7.16 Theorem is INTEGRA7:31 or MESFUN10:21. Corollary No reference. Uniform Convergence and Differentiation 7.17 Theorem No reference. #TODO show that 7.18 Theorem No reference. #TODO existence of continuous nowhere differentiable function Equicontinuous Families of Functions 7.19 Definition No reference for pointwise bounded, but for F is uniformly_bounded (MESFUN10:def 1). 7.20 Example No reference. 7.21 Example No reference. 7.22 Definition No reference. 7.23 Theorem No reference. 7.24 Theorem No reference. 7.25 Theorem No reference. The Stone-Weierstrass Theorem 7.26 Theorem No reference #TODO the Stone-Weierstrass theorem 7.27 Corollary No reference. 7.28 Definition The algebra of complex functions on a domain is CAlgebra(E) (CFUNCDOM:def 8), the real analogon of that is RAlgebra(E) (FUNCSDOM:def 9). A general algebra structure is found in POLYALG (not to be confused with the universal algebra from UNIALG_1). Subalgebras for complex algebras are defined in CC0SP1:def 1, for real algebras in C0SP1:def 9. No reference for uniformly closed or uniformly closure. 7.29 Theorem No reference. 7.30 Definition No reference. 7.31 Theorem No reference. 7.32 Theorem No reference. 7.33 Theorem No reference. Exercises 1. No reference. 2. No reference. 3. No reference. 4. No reference. 5. 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. 14. No reference. 15. No reference. 16. No reference. 17. No reference. 18. No reference. 19. No reference. 20. No reference. 21. No reference. 22. No reference. 23. No reference. 24. No reference. 25. No reference. 26. No reference.