ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints
theorem ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
A.SeparatesPoints → ∀ (f : C(X, ℝ)), f ∈ A.topologicalClosure
This theorem is an alternative statement of the Stone-Weierstrass theorem. It states that for any compact topological space 'X' and any subalgebra 'A' of the space of continuous real-valued functions on 'X' that separates points, every such continuous function 'f' can be approximated as closely as desired (in the uniform norm) by functions in 'A'. In other words, 'f' is an element of the topological closure of 'A'.
More concisely: Given a compact topological space X and a separating subalgebra A of continuous real-valued functions on X, every continuous function f on X can be uniformly approximated by functions in A.
|
ContinuousMap.algHom_ext_map_X
theorem ContinuousMap.algHom_ext_map_X :
∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : TopologicalSpace A] [inst_3 : T2Space A]
{s : Set ℝ} [inst_4 : CompactSpace ↑s] {φ ψ : C(↑s, ℝ) →ₐ[ℝ] A},
Continuous ⇑φ →
Continuous ⇑ψ →
φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) =
ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
φ = ψ
This theorem states that for any real algebra `A` with a ring structure and topology, such that `A` is a Hausdorff space (also known as a T2 space), and given a compact subset `s` of the real numbers, if we have two continuous algebra homomorphisms `φ` and `ψ` from the set of continuous functions from `s` to ℝ into `A`, and if these homomorphisms agree on the evaluation of the polynomial variable `X` (interpreted as a continuous map via the `Polynomial.toContinuousMapOnAlgHom` function), then the two homomorphisms `φ` and `ψ` are in fact equal. In other words, agreeing on how they map the polynomial variable `X` is enough to ensure that these two continuous algebra homomorphisms are the same.
More concisely: Given a Hausdorff topological real algebra `A` and compact subset `s` of the real numbers, if two continuous algebra homomorphisms from `s` to `A` agree on the evaluation of polynomials in `X`, then they are equal.
|
ContinuousMap.starAlgHom_ext_map_X
theorem ContinuousMap.starAlgHom_ext_map_X :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra 𝕜 A]
[inst_4 : TopologicalSpace A] [inst_5 : T2Space A] {s : Set 𝕜} [inst_6 : CompactSpace ↑s]
{φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A},
Continuous ⇑φ →
Continuous ⇑ψ →
φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) =
ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
φ = ψ
This theorem states that for any type `𝕜` that behaves like the field of real or complex numbers (has a `RCLike 𝕜` instance), a star ring `A` (a type with a Ring structure and a star operation), and a set `s` of elements from `𝕜`, if `φ` and `ψ` are continuous star algebra homomorphisms from the continuous functions `C(s, 𝕜)` into `A`, and if they agree at the polynomial variable `X` (when `X` is viewed as a continuous function via `Polynomial.toContinuousMapOnAlgHom s`), then `φ` and `ψ` are, in fact, equal. This essentially means that any two continuous star algebra homomorphisms that coincide at the polynomial variable are the same.
More concisely: If `𝕜` is a field with `RCLike 𝕜` instance, `A` is a star ring, `s` is a set of elements from `𝕜`, and `φ` and `ψ` are continuous star algebra homomorphisms from `C(s, 𝕜)` to `A` that agree on polynomials, then `φ = ψ`.
|
ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints
theorem ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
A.SeparatesPoints → ∀ (f : C(X, ℝ)) (ε : ℝ), 0 < ε → ∃ g, ‖↑g - f‖ < ε
This theorem is an alternate formulation of the Stone-Weierstrass theorem. It states that if `A` is a subalgebra of the set of all continuous real-valued functions on a topological space `X` (where `X` is additionally compact), and if `A` can separate points in `X`, then for every real-valued continuous function `f` on `X` and for any positive real number `ε`, there exists a function `g` in `A` such that the norm of the difference between `g` and `f` is less than `ε`. In other words, any continuous function can be approximated well by functions in the subalgebra `A`, provided `A` separates points.
More concisely: If `A` is a separable, compact subalgebra of continuous real-valued functions on a compact topological space `X`, then for every continuous real-valued function `f` on `X` and for any `ε > 0`, there exists a function `g` in `A` with `∥g - f∥ < ε`.
|
polynomialFunctions.starClosure_topologicalClosure
theorem polynomialFunctions.starClosure_topologicalClosure :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : CompactSpace ↑s],
(polynomialFunctions s).starClosure.topologicalClosure = ⊤
The theorem `polynomialFunctions.starClosure_topologicalClosure` states that for any compact set `s` of elements from a field `𝕜`, which is either the real numbers `ℝ` or the complex numbers `ℂ`, the topological closure of the star subalgebra generated by the polynomial functions on `s` is dense in the set of all continuous functions from `s` to `𝕜`. In other words, every continuous function from `s` to `𝕜` can be approximated arbitrarily closely by a polynomial function on `s`.
More concisely: The topological closure of the set of polynomial functions on a compact set in a field is dense in the space of all continuous functions from that set to the field.
|
ContinuousMap.polynomial_comp_attachBound_mem
theorem ContinuousMap.polynomial_comp_attachBound_mem :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A)
(g : Polynomial ℝ), (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A
This theorem states that given a continuous function `f` in a subalgebra `A` of the space of continuous real-valued functions on a topological space `X`, postcomposing `f` by a polynomial results in another function in `A`. More precisely, we view `f` as a function into a restricted target set `Set.Icc (-‖f‖) ‖f‖` (the closed interval from `-‖f‖` to `‖f‖`), and then postcompose this function with a polynomial function defined on this interval. The output, according to the theorem, also belongs to the subalgebra `A`. This theorem applies when `X` is a compact space.
More concisely: Given a compact topological space X, a continuous function f from X to R belonging to a subalgebra A of C(X), and a polynomial p, the composition of f and p belongs to A, where f is viewed as a function into the closed interval [−||f||, ||f||].
|
polynomialFunctions.topologicalClosure
theorem polynomialFunctions.topologicalClosure :
∀ (s : Set ℝ) [inst : CompactSpace ↑s], (polynomialFunctions s).topologicalClosure = ⊤
This theorem states that, given a compact set `s` of real numbers, the closure of the polynomial functions on `s` in the topology of continuous real-valued functions is the entire space of such functions. In other words, every continuous function on a compact set of real numbers can be approximated arbitrarily closely by polynomial functions. This is a generalization of the Weierstrass approximation theorem, and a specific case is given by `polynomialFunctions_closure_eq_top` when `s` is a closed and bounded interval `[a, b]`. The proof of this theorem could potentially be simplified by employing this special case.
More concisely: The closure of polynomial functions on a compact set of real numbers equals the space of all continuous real-valued functions on that set (Weierstrass approximation theorem).
|
ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints
theorem ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
A.SeparatesPoints → ∀ (f : X → ℝ), Continuous f → ∀ (ε : ℝ), 0 < ε → ∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε
This theorem is an alternative formulation of the Stone-Weierstrass theorem, which will appeal to those who prefer to work directly with epsilons and do not want to use the notion of bundled continuous functions.
In more detail, the theorem states that given any compact topological space `X` and a subalgebra `A` of the continuous functions from `X` to the real numbers, if `A` separates points in `X`, then for any real-valued continuous function `f` on `X`, and any positive real number `ε`, there exists a function `g` in the subalgebra such that the absolute difference between `g(x)` and `f(x)` is less than `ε` for all `x` in `X`. In other words, any real-valued continuous function on `X` can be approximated arbitrarily closely by functions from the subalgebra `A`.
More concisely: Given a compact topological space X and a subalgebra A of its continuous real-valued functions, if A separates points in X, then for every continuous real-valued function f on X and every ε > 0, there exists g in A such that |f(x) - g(x)| < ε for all x in X.
|
ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints
theorem ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
A.SeparatesPoints → A.topologicalClosure = ⊤
The theorem is a statement of the Stone-Weierstrass Approximation Theorem. In the context of compact topological spaces, this theorem states that if a subalgebra `A` of the continuous functions from `X` to the real numbers (`C(X, ℝ)`) has the property of separating points (`A.SeparatesPoints`), then the topological closure of this subalgebra is the entire set of continuous functions (`⊤`). In other words, any continuous function on `X` can be approximated as closely as desired by functions in `A`, provided that `A` separates points.
More concisely: If a subalgebra of continuous real-valued functions on a compact topological space separates points, then its closure equals the set of all continuous real-valued functions on that space.
|
ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints :
∀ {𝕜 : Type u_1} {X : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
(A : StarSubalgebra 𝕜 C(X, 𝕜)), A.SeparatesPoints → A.topologicalClosure = ⊤
This theorem, known as the Stone-Weierstrass approximation theorem for `RCLike` classes, states that for any star subalgebra `A` of `C(X, 𝕜)`, where `X` is a compact topological space and `𝕜` is a `RCLike` class, if `A` separates points then the topological closure of `A` is equal to the entire set of `C(X, 𝕜)`. In essence, this theorem asserts that for such spaces, the complex or real valued continuous functions on `X` which that satisfy the star property (i.e., they are star subalgebras) and are capable of distinguishing between different points on `X` are dense in the function space `C(X, 𝕜)`.
More concisely: If `A` is a star subalgebra of `C(X, 𝕜)` over a compact space `X` with respect to a `RCLike` class `𝕜`, then `A` is dense in `C(X, 𝕜)` if and only if `A` separates points.
|