# 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 | edit source]

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

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

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

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

**Corollary** No reference.

## Uniform Convergence and Differentiation[edit | edit source]

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

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

**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[edit | edit source]

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.