Universal approximation (nD, Stone–Weierstrass, Tensor vectors)

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 sanity check” in approximation theory:

On any compact set K ⊆ ℝⁿ, the subalgebra of continuous functions generated by the coordinate projections is dense in C(K,ℝ).

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

We phrase this for TorchLean’s vector tensors Tensor ℝ (.dim n .scalar), using the equivalence Tensor.dimScalarEquiv to transport the standard product topology.

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.

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximationND.TensorVec (n : ℕ) : Type

Shorthand for a length-n real vector tensor Tensor ℝ (.dim n .scalar).

@[implicit_reducible]

noncomputable instance NN.MLTheory.Proofs.UniversalApproximationND.TensorVec.instTopologicalSpace (n : ℕ) : TopologicalSpace (TensorVec n)

theorem NN.MLTheory.Proofs.UniversalApproximationND.TensorVec.continuous_toFun (n : ℕ) : Continuous (Spec.Tensor.dimScalarEquiv n).toFun

The tensor-to-function direction is continuous by construction of the induced topology.

theorem NN.MLTheory.Proofs.UniversalApproximationND.TensorVec.continuous_invFun (n : ℕ) : Continuous (Spec.Tensor.dimScalarEquiv n).invFun

The function-to-tensor inverse is continuous, so the tensor/vector equivalence is a homeomorphism.

noncomputable def NN.MLTheory.Proofs.UniversalApproximationND.TensorVec.homeomorph (n : ℕ) : TensorVec n ≃ₜ (Fin n → ℝ)

Homeomorphism between TorchLean tensor vectors and ordinary Fin n → ℝ vectors.

noncomputable def NN.MLTheory.Proofs.UniversalApproximationND.StoneWeierstrass.coord {n : ℕ} (K : Set (TensorVec n)) (i : Fin n) : C(↑K, ℝ)

Coordinate projection as a continuous map K → ℝ.

noncomputable def NN.MLTheory.Proofs.UniversalApproximationND.StoneWeierstrass.coordSubalg {n : ℕ} (K : Set (TensorVec n)) : Subalgebra ℝ C(↑K, ℝ)

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

theorem NN.MLTheory.Proofs.UniversalApproximationND.StoneWeierstrass.coordSubalg_separatesPoints {n : ℕ} (K : Set (TensorVec 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.UniversalApproximationND.StoneWeierstrass.coordSubalg_topologicalClosure_eq_top {n : ℕ} (K : Set (TensorVec 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.UniversalApproximationND.StoneWeierstrass.exists_coordSubalg_near_continuousMap {n : ℕ} (K : Set (TensorVec 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 ε > 0, produce a coordinate-polynomial-like continuous function within ε in sup norm.