Motivation: approximating entire continuous functions

An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. Polynomial approximation on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. Lebl, Theorem 11.7.1.

The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s Basic Analysis, Volume II. Source section.

Setting: function algebras and uniform error

A metric space is a set $X$ with a nonnegative, symmetric distance $d(x,y)$ that vanishes exactly when $x=y$ and satisfies the triangle inequality. It is compact if every cover by open sets has a finite subcover. Let $K$ be either the real numbers $\mathbb R$ or the complex numbers $\mathbb C$, and write $C(X,K)$ for the continuous functions from $X$ to $K$. Products, sums, and scalar multiplication of functions are taken pointwise. The notation $K[t]$ denotes polynomials in one indeterminate $t$ with coefficients in $K$, and $[a,b]=\{x\in\mathbb R:a\le x\le b\}$ for real endpoints $a,b$.

A non-unital function algebra $A$ contains the zero function and is closed under these three operations. It need not contain the constant function $1$. It separates points if, whenever $x\ne y$, some $g\in A$ satisfies $g(x)\ne g(y)$. It vanishes nowhere if, for each $x$, some $g\in A$ satisfies $g(x)\ne0$. The witness may depend on $x$; one everywhere nonzero function is not specified. A complex algebra is self-adjoint if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15.

Uniform convergence of $f_n$ to $f$ means

$$\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall n\ge N\;\forall x\in X, \qquad |f_n(x)-f(x)|<\varepsilon.$$

Here $|\cdot|$ is real absolute value or complex modulus. On compact $X$, the closure $\overline A$ in $C(X,K)$ uses this uniform topology; saying that $A$ is dense means $\overline A=C(X,K)$. Mathlib’s compact-domain convergence interface.

Formalization targets

The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.

Theorem 11.7.1. For $K=\mathbb R$ and for $K=\mathbb C$, respectively,

$$f\in C([a,b],K)\Longrightarrow \exists(p_n)_{n\in\mathbb N}\subseteq K[t],\qquad p_n\longrightarrow f\ \text{uniformly on }[a,b].$$

The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. Source theorem.

Corollary 11.7.4. For $a\ge0$,

$$\exists(p_n)\subseteq\mathbb R[t],\qquad (\forall n,\ p_n(0)=0)\ \land\ p_n\longrightarrow |\cdot|\ \text{uniformly on }[-a,a].$$

Source corollary.

Proposition 11.7.6. For compact metric $X$ and either scalar field,

$$A\text{ a non-unital algebra in }C(X,K) \Longrightarrow\overline A\text{ is such an algebra}.$$

Source proposition.

Proposition 11.7.11. For an arbitrary set $X$, without topology, let $A\subseteq K^X$ be an algebra separating points and vanishing nowhere. Then

$$\forall x\ne y\;\forall c,d\in K\;\exists f\in A, \qquad f(x)=c\ \land\ f(y)=d.$$

Both scalar fields belong to this single target. Source proposition.

Theorem 11.7.12. For compact metric $X$,

$$A\subseteq C(X,\mathbb R)\text{ an algebra separating points and vanishing nowhere} \Longrightarrow\overline A=C(X,\mathbb R).$$

Source theorem.

Theorem 11.7.16, complex Stone–Weierstrass. For compact metric $X$,

$$\begin{gathered} A\subseteq C(X,\mathbb C)\text{ a self-adjoint algebra},\\ A\text{ separates points and vanishes nowhere} \end{gathered} \Longrightarrow\overline A=C(X,\mathbb C).$$

Source theorem.

Significance: density without an assumed unit

The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.

These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. Polynomial approximation, Stone–Weierstrass library.

Difficulty: local distinctions do not give uniform control

Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.

Requiring $1\in A$ would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. Library theorem hypotheses.

Formalization scope

Namespace LeblRA uses NonUnitalSubalgebra, ContinuousMap, real and complex polynomials, TendstoUniformly, and topological closure. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise star operation on complex continuous maps.

The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes $a\ge0$ and includes $a=0$. Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.

Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. Non-unital algebra structures, topological closures.

Selected references

• Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume II, author-published open textbook, version 6.3, 2026, §11.7. Section text; edition information.
• The Mathlib community, Mathlib, Lean mathematical library, revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. Polynomial approximation, Stone–Weierstrass and zero-preserving continuous maps, non-unital algebra closures.