Stone–Weierstrass Approximation for Tensor Inputs

This file does not prove the classical neural network universal approximation theorem (Cybenko/Hornik/Leshno, etc.). That result is substantially more work to mechanize.

What we do prove here is a standard expressivity theorem in approximation theory:

On any compact set $K\subseteq\mathbb{R}^n$, the subalgebra of continuous functions generated by the coordinate projections is dense in $C(K,\mathbb{R})$.

Equivalently: functions on a compact set can be uniformly approximated by polynomial expressions in the coordinates (Stone–Weierstrass).

We phrase this for TorchLean’s rank-one tensors Tensor ℝ [n] with the Euclidean metric topology from NN.Proofs.Tensor.Euclidean; no separate induced topology is installed. The coordinate projections are read through the linear equivalence Tensor.vectorEquiv, which is continuous by Tensor.continuous_vectorEquiv.

This module is therefore a topology/approximation bridge, not a claim about one particular neural architecture. The cited classical lineage is Stone--Weierstrass for polynomial density, with the neural-network universal-approximation motivation coming from Cybenko, Hornik, Leshno et al., and Pinkus. The ReLU compact-set file uses this bridge as one ingredient when relating tensor-valued inputs to TorchLean network semantics.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.StoneWeierstrass.coord {n : ℕ} (K : Set (TorchLean.Tensor ℝ [n])) (i : Fin n) : C(↑K, ℝ)

Coordinate projection as a continuous map $K\to\mathbb{R}$.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.StoneWeierstrass.coordSubalg {n : ℕ} (K : Set (TorchLean.Tensor ℝ [n])) : Subalgebra ℝ C(↑K, ℝ)

Subalgebra generated by the coordinate projections on the compact tensor domain K.

theorem NN.MLTheory.Proofs.UniversalApproximation.StoneWeierstrass.coordSubalg_separatesPoints {n : ℕ} (K : Set (TorchLean.Tensor ℝ [n])) : (coordSubalg K).SeparatesPoints

Coordinate functions separate points.

If two tensor points differ, the tensor/vector equivalence gives a coordinate where they differ, and that coordinate projection belongs to coordSubalg.

theorem NN.MLTheory.Proofs.UniversalApproximation.StoneWeierstrass.coordSubalg_topologicalClosure_eq_top {n : ℕ} (K : Set (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] : (coordSubalg K).topologicalClosure = ⊤

Stone--Weierstrass closure theorem for the coordinate-generated subalgebra.

On a compact set, a subalgebra of continuous real-valued functions that separates points has dense topological closure. Here the coordinate projections provide the separation witness.

theorem NN.MLTheory.Proofs.UniversalApproximation.StoneWeierstrass.exists_coordSubalg_near_continuousMap {n : ℕ} (K : Set (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] (f : C(↑K, ℝ)) (ε : ℝ) (hε : 0 < ε) : ∃ (g : ↥(coordSubalg K)), ‖↑g - f‖ < ε

Approximate any continuous scalar function on $K$ by an element of the coordinate-generated subalgebra.

This is the operational form used downstream: given $\varepsilon>0$, produce a coordinate-polynomial-like continuous function within $\varepsilon$ in the supremum norm.