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 {α : Type} [TorchLean.Storage α] (t : TorchLean.Tensor α [1]) : α

Extract the unique entry of 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 {n hidDim : ℕ} (l1 : Spec.LinearSpec ℝ n hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1) (x : TorchLean.Tensor ℝ [n]) : 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.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.grid (a δ : ℝ) (k : ℕ) : ℝ

The uniform grid with left endpoint a and spacing δ.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.grid_zero (a δ : ℝ) : grid a δ 0 = a

The uniform grid starts at its left endpoint.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.grid_step (a δ : ℝ) (k : ℕ) : grid a δ (k + 1) - grid a δ k = δ

Consecutive grid points are one mesh width apart.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.grid_mono (a : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) : Monotone (grid a δ)

Nonnegative spacing gives an ordered grid.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.slope (δ : ℝ) (y : ℕ → ℝ) (k : ℕ) : ℝ

The slope between consecutive, arbitrary sample values.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.coefficient (δ : ℝ) (y : ℕ → ℝ) : ℕ → ℝ

Hinge coefficients are the initial slope followed by successive slope differences.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.slope_mul_step {δ : ℝ} (hδ : δ ≠ 0) (y : ℕ → ℝ) (k : ℕ) : slope δ y k * δ = y (k + 1) - y k

The slope times a nonzero mesh width is the corresponding sample increment.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.sum_coefficient (δ : ℝ) (y : ℕ → ℝ) (k : ℕ) : ∑ i ∈ Finset.range (k + 1), coefficient δ y i = slope δ y k

Summing the slope differences recovers the slope of the last segment.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.interpolant (N : ℕ) (a δ : ℝ) (y : ℕ → ℝ) (x : ℝ) : ℝ

The width-N hinge interpolant of the samples y 0, …, y N.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.affine_on_segment {N k : ℕ} {a δ x : ℝ} (y : ℕ → ℝ) (hδ : 0 ≤ δ) (hkN : k + 1 ≤ N) (hx0 : grid a δ k ≤ x) (hx1 : x ≤ grid a δ (k + 1)) : interpolant N a δ y x = interpolant N a δ y (grid a δ k) + slope δ y k * (x - grid a δ k)

On each grid cell, the hinge sum is affine with the prescribed sample slope.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.interpolant_grid {N : ℕ} (a : ℝ) {δ : ℝ} (y : ℕ → ℝ) (hδ : 0 < δ) (k : ℕ) (hk : k ≤ N) : interpolant N a δ y (grid a δ k) = y k

Positive spacing makes the hinge interpolant exact at every bounded grid point.

theorem NN.MLTheory.Proofs.UniversalApproximation.Internal.UniformInterpolation.hinge_fun_eq_interpolant (N : ℕ) (a δ : ℝ) (y : ℕ → ℝ) (x : ℝ) : hingeFun N (fun (i : Fin N) => grid a δ ↑i) (fun (i : Fin N) => coefficient δ y ↑i) (y 0) x = interpolant N a δ y x

The finite-index hinge network and the range-sum interpolant have the same value.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_hinge_approximation_Icc_of_mesh {f : ℝ → ℝ} {a b L ε : ℝ} {N : ℕ} (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|) (hNpos_nat : 0 < N) (hmesh : 2 * L * ((b - a) / ↑N) < ε) : ∃ (t : Fin N → ℝ) (c : Fin N → ℝ), ∀ x ∈ Set.Icc a b, |f x - hingeFun N t c (f a) x| < ε

A uniform mesh with N cells gives a width-N hinge approximation whenever 2 * L * ((b - a) / N) is below the requested error. The same interpolant serves both the qualitative existence theorem and the theorem with an explicit width.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.reluApproximationWidth (L a b ε : ℝ) : ℕ

Explicit hidden width for the 1D Lipschitz ReLU approximation construction.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_approximation_width_pos (L a b ε : ℝ) : 0 < reluApproximationWidth L a b ε

The explicit ReLU approximation width is always positive.

theorem NN.MLTheory.Proofs.UniversalApproximation.two_mul_mul_sub_div_relu_approximation_width_lt {L a b ε : ℝ} (hε : 0 < ε) : 2 * L * (b - a) / ↑(reluApproximationWidth L a b ε) < ε

The chosen width makes the mesh-size error term smaller than the target accuracy.

This is the arithmetic heart of the explicit-rate theorem: the ceiling construction ensures $N>2L(b-a)/\varepsilon$, hence $2L(b-a)/N<\varepsilon$.

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.