Documentation

Mathlib.Topology.ContinuousMap.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.

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.

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

Equations
  • f.attachBound = { toFun := fun (x : X) => f x, , continuous_toFun := }
Instances For
    @[simp]
    theorem ContinuousMap.attachBound_apply_coe {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (f : C(X, )) (x : X) :
    (f.attachBound x) = f x
    theorem ContinuousMap.polynomial_comp_attachBound {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (f : A) (g : Polynomial ) :
    (g.toContinuousMapOn (Set.Icc (-f) f)).comp (↑f).attachBound = ((Polynomial.aeval f) g)
    theorem ContinuousMap.polynomial_comp_attachBound_mem {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (f : A) (g : Polynomial ) :
    (g.toContinuousMapOn (Set.Icc (-f) f)).comp (↑f).attachBound 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} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (f : A) (p : C((Set.Icc (-f) f), )) :
    p.comp (↑f).attachBound A.topologicalClosure
    theorem ContinuousMap.abs_mem_subalgebra_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (f : A) :
    |f| A.topologicalClosure
    theorem ContinuousMap.inf_mem_subalgebra_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (f : A) (g : A) :
    f g A.topologicalClosure
    theorem ContinuousMap.inf_mem_closed_subalgebra {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (h : IsClosed A) (f : A) (g : A) :
    f g A
    theorem ContinuousMap.sup_mem_subalgebra_closure {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (f : A) (g : A) :
    f g A.topologicalClosure
    theorem ContinuousMap.sup_mem_closed_subalgebra {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (h : IsClosed A) (f : A) (g : A) :
    f g A
    theorem ContinuousMap.sublattice_closure_eq_top {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (L : Set C(X, )) (nA : L.Nonempty) (inf_mem : fL, gL, f g L) (sup_mem : fL, gL, f g L) (sep : L.SeparatesPointsStrongly) :
    theorem ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (w : A.SeparatesPoints) :
    A.topologicalClosure =

    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 ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (w : A.SeparatesPoints) (f : C(X, )) :
    f A.topologicalClosure

    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} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (w : A.SeparatesPoints) (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 ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra C(X, )) (w : A.SeparatesPoints) (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.

    theorem Subalgebra.SeparatesPoints.rclike_to_real {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [TopologicalSpace X] {A : StarSubalgebra 𝕜 C(X, 𝕜)} (hA : A.SeparatesPoints) :
    (Subalgebra.comap (AlgHom.compLeftContinuous RCLike.ofRealAm ) (Subalgebra.restrictScalars A.toSubalgebra)).SeparatesPoints

    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_1} {X : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] (A : StarSubalgebra 𝕜 C(X, 𝕜)) (hA : A.SeparatesPoints) :
    A.topologicalClosure =

    The Stone-Weierstrass approximation theorem, RCLike version, that a star subalgebra A of C(X, 𝕜), where X is a compact topological space and RCLike 𝕜, is dense if it separates 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} [RCLike 𝕜] (s : Set 𝕜) [CompactSpace s] :
    (polynomialFunctions s).starClosure.topologicalClosure =

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

    theorem ContinuousMap.induction_on {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} {p : C(s, 𝕜)Prop} (const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) (id : p (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) (star_id : p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))) (add : ∀ (f g : C(s, 𝕜)), p fp gp (f + g)) (mul : ∀ (f g : C(s, 𝕜)), p fp gp (f * g)) (closure : (∀ f(polynomialFunctions s).starClosure, p f)∀ (f : C(s, 𝕜)), p f) (f : C(s, 𝕜)) :
    p f

    An induction principle for C(s, 𝕜).

    theorem ContinuousMap.induction_on_of_compact {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [CompactSpace s] {p : C(s, 𝕜)Prop} (const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) (id : p (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) (star_id : p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))) (add : ∀ (f g : C(s, 𝕜)), p fp gp (f + g)) (mul : ∀ (f g : C(s, 𝕜)), p fp gp (f * g)) (frequently : ∀ (f : C(s, 𝕜)), (∃ᶠ (g : C(s, 𝕜)) in nhds f, p g)p f) (f : C(s, 𝕜)) :
    p f
    theorem ContinuousMap.algHom_ext_map_X {A : Type u_1} [Ring A] [Algebra A] [TopologicalSpace A] [T2Space A] {s : Set } [CompactSpace s] {φ : C(s, ) →ₐ[] A} {ψ : C(s, ) →ₐ[] A} (hφ : Continuous φ) (hψ : Continuous ψ) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) 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} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [T2Space A] {s : Set 𝕜} [CompactSpace s] {φ : C(s, 𝕜) →⋆ₐ[𝕜] A} {ψ : C(s, 𝕜) →⋆ₐ[𝕜] A} (hφ : Continuous φ) (hψ : Continuous ψ) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) 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.

    Continuous maps sending zero to zero #

    theorem ContinuousMap.AlgHom.closure_ker_inter {F : Type u_2} {S : Type u_3} {K : Type u_4} {A : Type u_5} [CommRing K] [Ring A] [Algebra K A] [TopologicalSpace K] [T1Space K] [TopologicalSpace A] [ContinuousSub A] [ContinuousSMul K A] [FunLike F A K] [AlgHomClass F K A K] [SetLike S A] [OneMemClass S A] [AddSubgroupClass S A] [SMulMemClass S K A] (φ : F) (hφ : Continuous φ) (s : S) :
    closure (s (RingHom.ker φ)) = closure s (RingHom.ker φ)
    theorem ContinuousMapZero.adjoin_id_dense {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [Zero s] (h0 : 0 = 0) [CompactSpace s] :

    If s : Set 𝕜 with RCLike 𝕜 is compact and contains 0, then the non-unital star subalgebra generated by the identity function in C(s, 𝕜)₀ is dense. This can be seen as a version of the Weierstrass approximation theorem.

    theorem ContinuousMapZero.induction_on {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [Zero s] (h0 : 0 = 0) {p : ContinuousMapZero (↑s) 𝕜Prop} (zero : p 0) (id : p (ContinuousMapZero.id h0)) (star_id : p (star (ContinuousMapZero.id h0))) (add : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p fp gp (f + g)) (mul : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p fp gp (f * g)) (smul : ∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p fp (r f)) (closure : (∀ fNonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id h0}, p f)∀ (f : ContinuousMapZero (↑s) 𝕜), p f) (f : ContinuousMapZero (↑s) 𝕜) :
    p f

    An induction principle for C(s, 𝕜)₀.

    theorem ContinuousMapZero.induction_on_of_compact {𝕜 : Type u_1} [RCLike 𝕜] {s : Set 𝕜} [Zero s] (h0 : 0 = 0) [CompactSpace s] {p : ContinuousMapZero (↑s) 𝕜Prop} (zero : p 0) (id : p (ContinuousMapZero.id h0)) (star_id : p (star (ContinuousMapZero.id h0))) (add : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p fp gp (f + g)) (mul : ∀ (f g : ContinuousMapZero (↑s) 𝕜), p fp gp (f * g)) (smul : ∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p fp (r f)) (frequently : ∀ (f : ContinuousMapZero (↑s) 𝕜), (∃ᶠ (g : ContinuousMapZero (↑s) 𝕜) in nhds f, p g)p f) (f : ContinuousMapZero (↑s) 𝕜) :
    p f
    theorem ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [TopologicalSemiring A] [T2Space A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] {s : Set 𝕜} [Zero s] [CompactSpace s] (h0 : 0 = 0) (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : φ (ContinuousMapZero.id h0) * a = 0) (hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0) (hφ : Continuous φ) (f : ContinuousMapZero (↑s) 𝕜) :
    φ f * a = 0
    theorem ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [TopologicalSemiring A] [T2Space A] [Module 𝕜 A] [SMulCommClass 𝕜 A A] {s : Set 𝕜} [Zero s] [CompactSpace s] (h0 : 0 = 0) (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : a * φ (ContinuousMapZero.id h0) = 0) (hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0) (hφ : Continuous φ) (f : ContinuousMapZero (↑s) 𝕜) :
    a * φ f = 0