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 problemEdit

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 ConvergenceEdit

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 ContinuityEdit

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 IntegrationEdit

7.16 Theorem is INTEGRA7:31 or MESFUN10:21.

Corollary No reference.

Uniform Convergence and DifferentiationEdit

7.17 Theorem No reference. #TODO show that  

7.18 Theorem No reference. #TODO existence of continuous nowhere differentiable function

Equicontinuous Families of FunctionsEdit

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 TheoremEdit

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.

ExercisesEdit

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.