# Documentation

Mathlib.Topology.ContinuousFunction.StoneWeierstrass

# The Stone-Weierstrass theorem #

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.topologicalClosure. This follows from the Weierstrass approximation theorem on [-‖f‖, ‖f‖] by approximating abs uniformly thereon by polynomials.
• This ensures that A.topologicalClosure 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.topologicalClosure 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 star 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).

## Future work #

Extend to cover the case of subalgebras of the continuous functions vanishing at infinity, on non-compact spaces.

def ContinuousMap.attachBound {X : Type u_1} [] [] (f : ) :

Turn a function f : C(X, ℝ) into a continuous map into Set.Icc (-‖f‖) (‖f‖), thereby explicitly attaching bounds.

Instances For
@[simp]
theorem ContinuousMap.attachBound_apply_coe {X : Type u_1} [] [] (f : ) (x : X) :
↑() = f x
theorem ContinuousMap.polynomial_comp_attachBound {X : Type u_1} [] [] (A : ) (f : { x // x A }) (g : ) :
= ↑(↑() g)
theorem ContinuousMap.polynomial_comp_attachBound_mem {X : Type u_1} [] [] (A : ) (f : { x // x A }) (g : ) :
A

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.

theorem ContinuousMap.comp_attachBound_mem_closure {X : Type u_1} [] [] (A : ) (f : { x // x A }) (p : C(↑(Set.Icc (-f) f), )) :
theorem ContinuousMap.abs_mem_subalgebra_closure {X : Type u_1} [] [] (A : ) (f : { x // x A }) :
theorem ContinuousMap.inf_mem_subalgebra_closure {X : Type u_1} [] [] (A : ) (f : { x // x A }) (g : { x // x A }) :
f g
theorem ContinuousMap.inf_mem_closed_subalgebra {X : Type u_1} [] [] (A : ) (h : IsClosed A) (f : { x // x A }) (g : { x // x A }) :
f g A
theorem ContinuousMap.sup_mem_subalgebra_closure {X : Type u_1} [] [] (A : ) (f : { x // x A }) (g : { x // x A }) :
f g
theorem ContinuousMap.sup_mem_closed_subalgebra {X : Type u_1} [] [] (A : ) (h : IsClosed A) (f : { x // x A }) (g : { x // x A }) :
f g A
theorem ContinuousMap.sublattice_closure_eq_top {X : Type u_1} [] [] (L : Set ) (nA : ) (inf_mem : ∀ (f : ), f L∀ (g : ), g Lf g L) (sup_mem : ∀ (f : ), f L∀ (g : ), g Lf g L) (sep : ) :

The Stone-Weierstrass Approximation Theorem, that a subalgebra A of C(X, ℝ), where X is a compact topological space, is dense if it separates points.

An alternative statement of the Stone-Weierstrass theorem.

If A is a subalgebra of C(X, ℝ) which separates points (and X is compact), every real-valued continuous function on X is a uniform limit of elements of A.

theorem ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints {X : Type u_1} [] [] (A : ) (w : ) (f : ) (ε : ) (pos : 0 < ε) :
g, g - f < ε

An alternative statement of the Stone-Weierstrass theorem, for those who like their epsilons.

If A is a subalgebra of C(X, ℝ) which separates points (and X is compact), every real-valued continuous function on X is within any ε > 0 of some element of A.

theorem ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints {X : Type u_1} [] [] (A : ) (w : ) (f : X) (c : ) (ε : ) (pos : 0 < ε) :
g, ∀ (x : X), g x - f x < ε

An alternative statement of the Stone-Weierstrass theorem, for those who like their epsilons and don't like bundled continuous functions.

If A is a subalgebra of C(X, ℝ) which separates points (and X is compact), every real-valued continuous function on X is within any ε > 0 of some element of A.

theorem Subalgebra.SeparatesPoints.isROrC_to_real {𝕜 : Type u_2} {X : Type u_1} [] [] {A : } (hA : Subalgebra.SeparatesPoints A.toSubalgebra) :

If a star subalgebra of C(X, 𝕜) separates points, then the real subalgebra of its purely real-valued elements also separates points.

theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints {𝕜 : Type u_2} {X : Type u_1} [] [] [] (A : ) (hA : Subalgebra.SeparatesPoints A.toSubalgebra) :

The Stone-Weierstrass approximation theorem, IsROrC version, that a star subalgebra A of C(X, 𝕜), where X is a compact topological space and IsROrC 𝕜, is dense if itseparates points.

Polynomial functions in are dense in C(s, ℝ) when s is compact.

See polynomialFunctions_closure_eq_top for the special case s = Set.Icc a b which does not use the full Stone-Weierstrass theorem. Of course, that version could be used to prove this one as well.

theorem polynomialFunctions.starClosure_topologicalClosure {𝕜 : Type u_1} [] (s : Set 𝕜) [] :

The star subalgebra generated by polynomials functions is dense in C(s, 𝕜) when s is compact and 𝕜 is either ℝ or ℂ.

theorem ContinuousMap.algHom_ext_map_X {A : Type u_1} [Ring A] [] [] [] {s : } [] {φ : C(s, ) →ₐ[] A} {ψ : C(s, ) →ₐ[] A} (hφ : ) (hψ : ) (h : φ (↑() Polynomial.X) = ψ (↑() Polynomial.X)) :
φ = ψ

Continuous algebra homomorphisms from C(s, ℝ) into an ℝ-algebra A which agree at X : 𝕜[X] (interpreted as a continuous map) are, in fact, equal.

theorem ContinuousMap.starAlgHom_ext_map_X {𝕜 : Type u_1} {A : Type u_2} [] [Ring A] [] [Algebra 𝕜 A] [] [] {s : Set 𝕜} [] {φ : C(s, 𝕜) →⋆ₐ[𝕜] A} {ψ : C(s, 𝕜) →⋆ₐ[𝕜] A} (hφ : ) (hψ : ) (h : φ (↑() Polynomial.X) = ψ (↑() Polynomial.X)) :
φ = ψ

Continuous star algebra homomorphisms from C(s, 𝕜) into a star 𝕜-algebra A which agree at X : 𝕜[X] (interpreted as a continuous map) are, in fact, equal.