mathlib documentation

topology.continuous_function.stone_weierstrass

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.

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).

Future work #

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

noncomputable def continuous_map.attach_bound {X : Type u_1} [topological_space X] [compact_space X] (f : C(X, )) :

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

Equations
@[simp]
theorem continuous_map.attach_bound_apply_coe {X : Type u_1} [topological_space X] [compact_space X] (f : C(X, )) (x : X) :

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 continuous_map.sublattice_closure_eq_top {X : Type u_1} [topological_space X] [compact_space X] (L : set C(X, )) (nA : L.nonempty) (inf_mem : ∀ (f : C(X, )), f L∀ (g : C(X, )), g Lf g L) (sup_mem : ∀ (f : C(X, )), f L∀ (g : C(X, )), g Lf g L) (sep : L.separates_points_strongly) :

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.

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 continuous_map.exists_mem_subalgebra_near_continuous_of_separates_points {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra C(X, )) (w : A.separates_points) (f : X → ) (c : continuous f) (ε : ) (pos : 0 < ε) :
∃ (g : A), ∀ (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.

def continuous_map.conj_invariant_subalgebra {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [topological_space X] (A : subalgebra C(X, 𝕜)) :
Prop

A real subalgebra of C(X, 𝕜) is conj_invariant, if it contains all its conjugates.

Equations

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

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.