Commit 2021-05-01 20:07 ea379b09View on Github →
feat(topology/continuous_function): the Stone-Weierstrass theorem (#7305)
The Stone-Weierstrass theorem
If a subalgebra
C(X, ℝ), where
X is a compact Hausdorff space,
separates points, then it is dense.
We argue as follows.
- In any subalgebra
C(X, ℝ), if
f ∈ A, then
abs f ∈ A.topological_closure. This follows from the Weierstrass approximation theorem on
[-∥f∥, ∥f∥]by approximating
absuniformly thereon by polynomials.
- This ensures that
A.topological_closureis actually a sublattice: if it contains
g, then it contains the pointwise supremum
f ⊔ gand the pointwise infimum
f ⊓ g.
- Any nonempty sublattice
C(X, ℝ)which separates points is dense, by a nice argument approximating a given
fabove and below using separating functions. For each
x y : X, we pick a function
g x y ∈ Lso
g x y x = f xand
g x y y = f y. By continuity these functions remain close to
fon small patches around
y. We use compactness to identify a certain finitely indexed infimum of finitely indexed supremums which is then close to
feverywhere, obtaining the desired approximation.
- Finally we put these pieces together.
L = A.topological_closureis a nonempty sublattice which separates points since
Adoes, and so is dense (in fact equal to
Prove the complex version for self-adjoint subalgebras
A, by separately approximating
the real and imaginary parts using the real subalgebra of real-valued functions in
(which still separates points, by taking the norm-square of a separating function).
Extend to cover the case of subalgebras of the continuous functions vanishing at infinity,
on non-compact Hausdorff spaces.