# 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

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

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

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

edit**7.16 Theorem** is `INTEGRA7:31` or `MESFUN10:21`.

**Corollary** No reference.

## Uniform Convergence and Differentiation

edit**7.17 Theorem** No reference. #TODO show that

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

## Equicontinuous Families of Functions

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

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

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