THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
If a subalgebra A of C(X, ℝ), where X is a compact topological space,
separates points, then it is dense.
We argue as follows.
In any subalgebra A of C(X, ℝ), if f ∈ A, then abs f ∈ A.topological_closure.
This follows from the Weierstrass approximation theorem on [-‖f‖, ‖f‖] by
approximating abs uniformly thereon by polynomials.
This ensures that A.topological_closure is actually a sublattice:
if it contains f and g, then it contains the pointwise supremum f ⊔ g
and the pointwise infimum f ⊓ g.
Any nonempty sublattice L of C(X, ℝ) which separates points is dense,
by a nice argument approximating a given f above and below using separating functions.
For each x y : X, we pick a function g x y ∈ L so g x y x = f x and g x y y = f y.
By continuity these functions remain close to f on small patches around x and y.
We use compactness to identify a certain finitely indexed infimum of finitely indexed supremums
which is then close to f everywhere, obtaining the desired approximation.
Finally we put these pieces together. L = A.topological_closure is a nonempty sublattice
which separates points since A does, and so is dense (in fact equal to ⊤).
We then 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 A
(which still separates points, by taking the norm-square of a separating function).
Given a continuous function f in a subalgebra of C(X, ℝ), postcomposing by a polynomial
gives another function in A.
This lemma proves something slightly more subtle than this:
we take f, and think of it as a function into the restricted target set.Icc (-‖f‖) ‖f‖),
and then postcompose with a polynomial function on that interval.
This is in fact the same situation as above, and so also gives a function in A.
The Stone-Weierstrass approximation theorem, is_R_or_C version,
that a subalgebra A of C(X, 𝕜), where X is a compact topological space and is_R_or_C 𝕜,
is dense if it is conjugation-invariant and separates points.