Universal approximation (1D, explicit rate)

This file strengthens relu_universal_approximation_Icc by choosing an explicit hidden width in terms of the Lipschitz constant L, the interval length (b-a), and the target accuracy ε.

The bound is the standard O(1 / hidDim) rate coming from piecewise-linear interpolation: we pick

hidDim = ⌈(2 * L * (b - a)) / ε⌉ + 1,

which guarantees uniform approximation error < ε on Set.Icc a b.

Mathematically, this is the quantitative sibling of the constructive one-dimensional ReLU universal approximation proof in UniversalApproximation: sample a Lipschitz function on a uniform grid, interpolate linearly by hinge functions, and choose the grid fine enough that the Lipschitz modulus controls the interpolation error. The style is classical approximation theory (Pinkus) and agrees with the first-order rate used in modern ReLU-network approximation analyses such as Yarotsky's quantitative bounds.

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)/ε, hence 2L(b-a)/N < ε.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc_hinge_rate {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 → ∃ (t : Fin (reluApproximationWidth L a b ε) → ℝ) (c : Fin (reluApproximationWidth L a b ε) → ℝ), ∀ x ∈ Set.Icc a b, |f x - hingeFun (reluApproximationWidth L a b ε) t c (f a) x| < ε

Universal approximation (1D, hinge form) with an explicit width choice.

This is a quantitative variant of relu_universal_approximation_Icc_hinge where the hidden width is fixed to reluApproximationWidth L a b ε.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc_rate {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 → ∃ (l1 : Spec.LinearSpec ℝ 1 (reluApproximationWidth L a b ε)) (l2 : Spec.LinearSpec ℝ (reluApproximationWidth L a b ε) 1), ∀ x ∈ Set.Icc a b, |f x - mlpEval1d (reluApproximationWidth L a b ε) l1 l2 x| < ε

Universal approximation (1D, explicit rate) for a 2-layer ReLU MLP.

This is the MLP-packaged version of relu_universal_approximation_Icc_hinge_rate.