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 $F$ denote $\{f_{n}\}$. $F$ being pointwise convergent is described by F is_point_conv_on E (SEQFUNC:20, see also SEQFUNC:def 10). Then $\lim _{n\to \infty }f_{n}$ 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
$F$ being uniformly convergent on $E$ 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 $f'(x)=\lim _{n\to \infty }f_{n}(x)$

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 $E$ 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.