Motivation

Chapter 7 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) asks when a limit of functions inherits the properties of its members. Pointwise convergence preserves almost nothing: Rudin's opening examples give continuous $f_n$ with discontinuous limit, and sequences where $\lim_n \int f_n \ne \int \lim_n f_n$. Uniform convergence is the hypothesis that repairs this, and the chapter's second half asks the converse question — which functions arise as uniform limits from a given family — answered by the Stone–Weierstrass theorem (Theorem 7.32): an algebra of continuous real functions on a compact set that separates points and vanishes nowhere is uniformly dense in all continuous functions there.

The classical Weierstrass approximation theorem (7.26) — polynomials are dense in $C[a,b]$ — is the special case that made the general theorem worth proving, and is used in Chapter 8 for Fourier series and in Chapter 11 for the density of continuous functions in $L^2$.

This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral of Mission VI.

Setting

A sequence $f_n$ converges uniformly to $f$ on $E$ if for every $\varepsilon > 0$ there is $N$ with $|f_n(x) - f(x)| \le \varepsilon$ for all $n \ge N$ and all $x \in E$ — the same $N$ for every point. A family $\mathcal{F}$ is equicontinuous on $E$ if a single $\delta$ serves all its members in the definition of uniform continuity; it is pointwise bounded if each orbit $\{f(x) : f \in \mathcal{F}\}$ is bounded, and uniformly bounded if one bound works for all $f$ and all $x$.

A set $\mathcal{A}$ of real functions is an algebra if it is closed under addition, multiplication and multiplication by real scalars; it separates points on $K$ if for $x \ne y$ in $K$ some $f \in \mathcal{A}$ has $f(x) \ne f(y)$; it vanishes at no point of $K$ if for each $x \in K$ some $f \in \mathcal{A}$ has $f(x) \ne 0$. The uniform closure of $\mathcal{A}$ on $K$ is the set of uniform limits on $K$ of sequences from $\mathcal{A}$.

Formalization targets

Goal — Stone–Weierstrass (Theorem 7.32)

Let $K$ be compact and let $\mathcal{A}$ be an algebra of real continuous functions on $K$ which separates points on $K$ and vanishes at no point of $K$. Then

$$\overline{\mathcal{A}}^{\,\text{unif}} \supseteq C(K,\mathbb{R}) :$$

every continuous real function on $K$ is a uniform limit on $K$ of members of $\mathcal{A}$.

Milestones

$$\text{uniform convergence} \iff \text{uniform Cauchy criterion} \qquad (7.8)$$ $$|f_n| \le M_n \text{ on } E,\ \textstyle\sum M_n < \infty \Rightarrow \sum f_n \text{ converges uniformly} \qquad (7.10)$$ $$\lim_{t\to x}\lim_n f_n(t) = \lim_n \lim_{t \to x} f_n(t) \text{ under uniform convergence} \qquad (7.11)$$ $$\text{a uniform limit of continuous functions is continuous} \qquad (7.12)$$ $$f_n \in \mathcal{R}(\alpha),\ f_n \to f \text{ uniformly} \Rightarrow f \in \mathcal{R}(\alpha),\ \int f_n \, d\alpha \to \int f \, d\alpha \qquad (7.16)$$ $$f_n' \to h \text{ uniformly},\ f_n(x_0) \text{ convergent} \Rightarrow f_n \to g \text{ uniformly},\ g' = h \qquad (7.17)$$ $$\text{there is a continuous nowhere differentiable } f : \mathbb{R} \to \mathbb{R} \qquad (7.18)$$ $$\text{pointwise bounded} + \text{equicontinuous on compact} \Rightarrow \text{uniformly bounded, convergent subsequence} \qquad (7.24,\ 7.25)$$ $$\text{polynomials are uniformly dense in } C[a,b] \qquad (7.26)$$

Significance

Uniform convergence is the standard hypothesis under which limits commute with continuity, integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and 7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential, trigonometric and Gamma functions as uniform limits and differentiates them term by term on the strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of continuity: a uniform limit of piecewise-linear functions can fail to be differentiable anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the standard route to existence theorems for differential and integral equations.

Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of functions, applicable to trigonometric polynomials, polynomials in several variables, and Lipschitz algebras alike.

Mathlib contains a Stone–Weierstrass theorem for subalgebras of C(X, ℝ) on compact Hausdorff spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain sets of functions on a compact subset $K$ of a metric space, uniform closure defined by sequences — so that they can be used together with the Riemann–Stieltjes integral built in Mission VI, which is not part of the library.

Difficulty

Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from the algebra one first produces $|f|$ as a uniform limit of polynomials in $f$ (which needs the polynomial approximation of $\sqrt{t}$ on $[0,1]$ and so cannot be circular with Theorem 7.26), then maxima and minima of pairs, then functions matching prescribed values at two points, and only then the local-to-global patching over a finite subcover. Each step is short; keeping the uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.

Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point cannot approximate functions that do not, and one that fails to separate two points cannot approximate functions that distinguish them.

Formalization scope

Conventions fixed by this mission:

• Uniform convergence is Mathlib's TendstoUniformlyOn … atTop; complex-valued sequences are used where Rudin allows complex values.
• Algebras, separation, non-vanishing and uniform closure are the predicates Rudin.IsFunctionAlgebra, Rudin.SeparatesPointsOn, Rudin.VanishesAtNoPointOn, Rudin.UniformClosureOn, defined for sets of functions X → ℝ and a compact subset K. The goal's conclusion is membership in the uniform closure, i.e. the existence of an approximating sequence from the algebra.
• Equicontinuity and the two boundedness notions are Rudin.EquicontinuousOn, Rudin.PointwiseBoundedOn, Rudin.UniformlyBoundedOn, stated with explicit $\varepsilon$ and $\delta$ as in Definitions 7.19 and 7.22.
• Theorem 7.16 is stated for the Riemann–Stieltjes integral of Mission VI, not for a Mathlib integral, so the two missions compose.
• Theorem 7.26 is stated for complex-valued $f$ and polynomials with complex coefficients evaluated at real points, as in Rudin.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 7 (pp. 143–171).
• M. H. Stone, The generalized Weierstrass approximation theorem, Mathematics Magazine 21 (1948), 167–184 and 237–254. https://doi.org/10.2307/3029750