mathlib3 documentation

topology.continuous_function.stone_weierstrass

The Stone-Weierstrass theorem #

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

Future work #

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

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

C(X, ↥(set.Icc (-‖f‖) ‖f‖))

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

Equations

f.attach_bound = {to_fun := λ (x : X), ⟨⇑f x, _⟩, continuous_to_fun := _}

@[simp]

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

↑(⇑(f.attach_bound) x) = ⇑f x

theorem continuous_map.polynomial_comp_attach_bound {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (f : ↥A) (g : polynomial ℝ) :

(g.to_continuous_map_on (set.Icc (-‖f‖) ‖f‖)).comp ↑f.attach_bound = ↑(⇑(polynomial.aeval f) g)

theorem continuous_map.polynomial_comp_attach_bound_mem {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (f : ↥A) (g : polynomial ℝ) :

(g.to_continuous_map_on (set.Icc (-‖f‖) ‖f‖)).comp ↑f.attach_bound ∈ 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 continuous_map.comp_attach_bound_mem_closure {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (f : ↥A) (p : C(↥(set.Icc (-‖f‖) ‖f‖), ℝ )) :

p.comp ↑f.attach_bound ∈ A.topological_closure

theorem continuous_map.abs_mem_subalgebra_closure {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (f : ↥A) :

↑f.abs ∈ A.topological_closure

theorem continuous_map.inf_mem_subalgebra_closure {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (f g : ↥A) :

↑f ⊓ ↑g ∈ A.topological_closure

theorem continuous_map.inf_mem_closed_subalgebra {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (h : is_closed ↑A) (f g : ↥A) :

↑f ⊓ ↑g ∈ A

theorem continuous_map.sup_mem_subalgebra_closure {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (f g : ↥A) :

↑f ⊔ ↑g ∈ A.topological_closure

theorem continuous_map.sup_mem_closed_subalgebra {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (h : is_closed ↑A) (f g : ↥A) :

↑f ⊔ ↑g ∈ 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 ∈ L → f ⊓ g ∈ L) (sup_mem : ∀ (f : C(X, ℝ )), f ∈ L → ∀ (g : C(X, ℝ )), g ∈ L → f ⊔ g ∈ L) (sep : L.separates_points_strongly) :

closure L = ⊤

theorem continuous_map.subalgebra_topological_closure_eq_top_of_separates_points {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (w : A.separates_points) :

A.topological_closure = ⊤

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.

theorem continuous_map.continuous_map_mem_subalgebra_closure_of_separates_points {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (w : A.separates_points) (f : C(X, ℝ )) :

f ∈ A.topological_closure

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 continuous_map.exists_mem_subalgebra_near_continuous_map_of_separates_points {X : Type u_1} [topological_space X] [compact_space X] (A : subalgebra ℝ C(X, ℝ )) (w : A.separates_points) (f : C(X, ℝ )) (ε : ℝ) (pos : 0 < ε) :

∃ (g : ↥A), ‖↑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 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

continuous_map.conj_invariant_subalgebra A = (subalgebra.map (alg_hom.comp_left_continuous ℝ is_R_or_C.conj_ae.to_alg_hom continuous_map.conj_invariant_subalgebra._proof_7) A ≤ A)

theorem continuous_map.mem_conj_invariant_subalgebra {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [topological_space X] {A : subalgebra ℝ C(X, 𝕜)} (hA : continuous_map.conj_invariant_subalgebra A) {f : C(X, 𝕜)} (hf : f ∈ A) :

⇑(alg_hom.comp_left_continuous ℝ is_R_or_C.conj_ae.to_alg_hom _) f ∈ A

theorem continuous_map.subalgebra_conj_invariant {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [topological_space X] {S : set C(X, 𝕜)} (hS : ∀ (f : C(X, 𝕜)), f ∈ S → ⇑(alg_hom.comp_left_continuous ℝ is_R_or_C.conj_ae.to_alg_hom _) f ∈ S) :

continuous_map.conj_invariant_subalgebra (subalgebra.restrict_scalars ℝ (algebra.adjoin 𝕜 S))

If a set S is conjugation-invariant, then its 𝕜-span is conjugation-invariant.

theorem subalgebra.separates_points.is_R_or_C_to_real {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [topological_space X] {A : subalgebra 𝕜 C(X, 𝕜)} (hA : A.separates_points) (hA' : continuous_map.conj_invariant_subalgebra (subalgebra.restrict_scalars ℝ A)) :

(subalgebra.comap (alg_hom.comp_left_continuous ℝ is_R_or_C.of_real_am is_R_or_C.continuous_of_real) (subalgebra.restrict_scalars ℝ A)).separates_points

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

theorem continuous_map.subalgebra_is_R_or_C_topological_closure_eq_top_of_separates_points {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [topological_space X] [compact_space X] (A : subalgebra 𝕜 C(X, 𝕜)) (hA : A.separates_points) (hA' : continuous_map.conj_invariant_subalgebra (subalgebra.restrict_scalars ℝ A)) :

A.topological_closure = ⊤

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.