Universal approximation (1D, constructive)

On a compact interval $I=[a,b]$, any Lipschitz function $f:\mathbb{R}\to\mathbb{R}$ can be uniformly approximated by a single-hidden-layer ReLU network (a 2-layer MLP).

This file formalizes the classic constructive proof strategy:

• approximate $f$ by a polygonal function on a uniform grid,
• express that polygonal function as an affine term plus a finite sum of hinges $\operatorname{ReLU}(x-t_i)$,
• package the hinge representation as TorchLean's spec-level 2-layer MLP (NN.Spec.Models.Mlp).

Main result

• relu_universal_approximation_Icc: existence of a 2-layer ReLU MLP approximator on Set.Icc a b.

References

• Leshno, Lin, Pinkus, Schocken (1993), Multilayer feedforward networks with a nonpolynomial activation function can approximate any function.
• Yarotsky (2017), Error bounds for approximations with deep ReLU networks.
• Pinkus (1999), Approximation theory of the MLP model in neural networks.

@[reducible, inline]

noncomputable abbrev NN.MLTheory.Proofs.UniversalApproximation.relu (x : ℝ) : ℝ

Shorthand for relu in this development, using TorchLean’s spec semantics.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_sub_eq_of_le {x t : ℝ} (h : t ≤ x) : relu (x - t) = x - t

If the knot $t$ is to the left of $x$, then $\operatorname{ReLU}(x-t)=x-t$.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_sub_eq_zero_of_le {x t : ℝ} (h : x ≤ t) : relu (x - t) = 0

If $x$ is to the left of the knot $t$, then $\operatorname{ReLU}(x-t)=0$.

def NN.MLTheory.Proofs.UniversalApproximation.extractScalarOutput (t : TorchLean.Tensor ℝ [1]) : ℝ

Extract scalar from a length-1 tensor.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.mlpEvalScalar (hidDim : ℕ) (l1 : Spec.LinearSpec ℝ 1 hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1) (x : ℝ) : ℝ

Evaluate a 2-layer ReLU MLP on a scalar input.

theorem NN.MLTheory.Proofs.UniversalApproximation.mlp_forward_eq_linear_relu_linear {hidDim : ℕ} (l1 : Spec.LinearSpec ℝ 1 hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1) (x : TorchLean.Tensor ℝ [1]) : Examples.mlpForward l1 l2 x = have z1 := Spec.linearSpec l1 x; have a1 := Activation.reluSpec z1; Spec.linearSpec l2 a1

TorchLean's MLP forward pass is exactly $\operatorname{linear}\circ\operatorname{ReLU}\circ\operatorname{linear}$.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeLayer1 (n : ℕ) (t : Fin n → ℝ) : Spec.LinearSpec ℝ 1 n

First real hinge layer: hidden unit $i$ computes $x-t_i$ before ReLU.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeLayer2 (n : ℕ) (c : Fin n → ℝ) (b : ℝ) : Spec.LinearSpec ℝ n 1

Second real hinge layer: sum hidden activations with coefficients $c_i$ and bias $b$.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeFun (n : ℕ) (t c : Fin n → ℝ) (b x : ℝ) : ℝ

Real hinge network $b+\sum_i c_i\operatorname{ReLU}(x-t_i)$.

theorem NN.MLTheory.Proofs.UniversalApproximation.mat_vec_mul_spec_matrix_vector (n : ℕ) (c v : Fin n → ℝ) : Spec.matVecMulSpec (TorchLean.Tensor.matrix fun (x : Fin 1) (j : Fin n) => c j) (TorchLean.Tensor.dim fun (j : Fin n) => TorchLean.Tensor.scalar (v j)) = TorchLean.Tensor.dim fun (x : Fin 1) => TorchLean.Tensor.scalar (∑ j : Fin n, c j * v j)

Matrix-vector multiply for a one-row matrix is the expected finite dot product.

theorem NN.MLTheory.Proofs.UniversalApproximation.mat_vec_mul_spec_matrix_singleton (n : ℕ) (x : ℝ) : Spec.matVecMulSpec (TorchLean.Tensor.matrix fun (x : Fin n) (x_1 : Fin 1) => 1) (Spec.singleton x) = TorchLean.Tensor.dim fun (x_1 : Fin n) => TorchLean.Tensor.scalar x

Matrix-vector multiply by the all-ones column extracts the scalar input into every hidden unit.

theorem NN.MLTheory.Proofs.UniversalApproximation.mlp_eval_scalar_hinge (n : ℕ) (t c : Fin n → ℝ) (b x : ℝ) : mlpEvalScalar n (hingeLayer1 n t) (hingeLayer2 n c b) x = hingeFun n t c b x

The explicit two-layer network built from hingeLayer1 and hingeLayer2 computes hingeFun.

This is the main semantic bridge from the approximation-theory hinge representation to TorchLean's spec-level MLP model.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc_hinge {f : ℝ → ℝ} {a b L : ℝ} (h_ab : a < b) (hL : 0 < L) (h_lip : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ L * |x - y|) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (t : Fin hidDim → ℝ) (c : Fin hidDim → ℝ), ∀ x ∈ Set.Icc a b, |f x - hingeFun hidDim t c (f a) x| < ε

1D Universal Approximation (ReLU, one hidden layer).

This is the classic constructive proof: Lipschitz continuity on $[a,b]$, a uniform partition, and piecewise-linear interpolation, then represent the interpolant as a finite linear combination of hinges $\operatorname{ReLU}(x-t_i)$.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc {f : ℝ → ℝ} {a b L : ℝ} (h_ab : a < b) (hL : 0 < L) (h_lip : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ L * |x - y|) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (l1 : Spec.LinearSpec ℝ 1 hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1), ∀ x ∈ Set.Icc a b, |f x - mlpEvalScalar hidDim l1 l2 x| < ε

1D Universal Approximation (ReLU, one hidden layer), stated as an existence theorem for a 2-layer MLP.

This is a wrapper around relu_universal_approximation_Icc_hinge that instantiates the linear layers as the explicit hinge construction.