ReLU approximation on compact sets (nD)

Key theorems proved in this file:

• approxOnC_of_mem_coordSubalg: every coordinate-polynomial (coordSubalg) on a compact set K is uniformly approximable by a 2-layer ReLU MLP (in the sense ApproxOnC).
• relu_universal_approximation_compact: for compact K and any f : C(K,ℝ), f is uniformly approximable on K by a 2-layer ReLU MLP.

Dependencies:

• NN.MLTheory.Proofs.Approximation.Universal.UniversalApproximation (constructive 1D ReLU approximation).
• NN.MLTheory.Proofs.Approximation.Universal.UniversalApproximationND (Stone–Weierstrass density of coordinate polynomials on compact sets of tensor vectors).
• NN.MLTheory.Proofs.ReLU.Bridge.ReLUMlpBridge (lifting 1D MLP constructions to TensorVec n).

def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOn {n : ℕ} (D : Set (ReLUMlpBridge.TensorVec n)) (f : ReLUMlpBridge.TensorVec n → ℝ) : Prop

ApproxOn D f means: on the domain D, the scalar function f can be uniformly approximated by a single-hidden-layer ReLU MLP (mlp_eval_nd).

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOn.zero {n : ℕ} (D : Set (ReLUMlpBridge.TensorVec n)) : ApproxOn D fun (x : ReLUMlpBridge.TensorVec n) => 0

The zero function is uniformly approximable on any domain D.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOn.add {n : ℕ} {D : Set (ReLUMlpBridge.TensorVec n)} {f g : ReLUMlpBridge.TensorVec n → ℝ} (hf : ApproxOn D f) (hg : ApproxOn D g) : ApproxOn D fun (x : ReLUMlpBridge.TensorVec n) => f x + g x

If f and g are uniformly approximable on D, then so is f + g.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOn.smul {n : ℕ} {D : Set (ReLUMlpBridge.TensorVec n)} {f : ReLUMlpBridge.TensorVec n → ℝ} (c : ℝ) (hf : ApproxOn D f) : ApproxOn D fun (x : ReLUMlpBridge.TensorVec n) => c * f x

If f is uniformly approximable on D, then so is the scalar multiple c • f.

def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) (f : C(↑K, ℝ)) : Prop

ApproxOnC K f means: the continuous map f : C(K,ℝ) can be uniformly approximated (on K) by a single-hidden-layer ReLU MLP (mlp_eval_nd, evaluated on the underlying point x.1).

Closure properties

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC.zero {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) : ApproxOnC K 0

The zero continuous function is uniformly approximable on K.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC.add {n : ℕ} {K : Set (ReLUMlpBridge.TensorVec n)} {f g : C(↑K, ℝ)} (hf : ApproxOnC K f) (hg : ApproxOnC K g) : ApproxOnC K (f + g)

If f and g are uniformly approximable on K, then so is f + g.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC.smul {n : ℕ} {K : Set (ReLUMlpBridge.TensorVec n)} (c : ℝ) {f : C(↑K, ℝ)} (hf : ApproxOnC K f) : ApproxOnC K (c • f)

If f is uniformly approximable on K, then so is the scalar multiple c • f.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC.sum_finset {n : ℕ} {K : Set (ReLUMlpBridge.TensorVec n)} {ι : Type} (s : Finset ι) (f : ι → C(↑K, ℝ)) (hf : ∀ i ∈ s, ApproxOnC K (f i)) : ApproxOnC K (∑ i ∈ s, f i)

Finite sums preserve ApproxOnC (Finset-indexed).

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC.sum_fintype {n : ℕ} {K : Set (ReLUMlpBridge.TensorVec n)} {ι : Type} [Fintype ι] (f : ι → C(↑K, ℝ)) (hf : ∀ (i : ι), ApproxOnC K (f i)) : ApproxOnC K (∑ i : ι, f i)

Finite sums preserve ApproxOnC (Fintype-indexed).

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.coordSubalg_eq_range_aeval {n : ℕ} (K : Set (UniversalApproximationND.TensorVec n)) : UniversalApproximationND.StoneWeierstrass.coordSubalg K = (MvPolynomial.aeval (UniversalApproximationND.StoneWeierstrass.coord K)).range

Identify the Stone–Weierstrass coordinate subalgebra with the range of multivariate-polynomial evaluation.

This is a small algebraic normalization lemma used to connect coordinate polynomials to MvPolynomial syntax (aeval).

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.sgn (b : Bool) : ℝ

Sign associated to a Boolean: true ↦ +1, false ↦ -1.

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.signedProd {d : ℕ} (ε : Fin d → Bool) : ℝ

Product of signs for an assignment ε : Fin d → Bool.

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.signedSum {d : ℕ} (ε : Fin d → Bool) (u : Fin d → ℝ) : ℝ

Signed linear form ∑ i, sgn (ε i) * u i.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.sum_bool_sgn_pow (k : ℕ) : ∑ b : Bool, sgn b ^ k = 1 + (-1) ^ k

Closed form for ∑ b : Bool, (sgn b)^k.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.sum_bool_sgn_pow_even (k : ℕ) (hk : Even k) : ∑ b : Bool, sgn b ^ k = 2

For even exponents, ∑ b : Bool, (sgn b)^k = 2.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.sum_bool_sgn_pow_odd (k : ℕ) (hk : Odd k) : ∑ b : Bool, sgn b ^ k = 0

For odd exponents, ∑ b : Bool, (sgn b)^k = 0.

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.fiberCount {d : ℕ} (p : Fin d → Fin d) (j : Fin d) : ℕ

The cardinality of the fiber { i | p i = j } as a natural number.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.prod_sgn_comp_eq_prod_pow_fiberCount {d : ℕ} (p : Fin d → Fin d) (ε : Fin d → Bool) : ∏ i : Fin d, sgn (ε (p i)) = ∏ j : Fin d, sgn (ε j) ^ fiberCount p j

Rewrite ∏ i, sgn (ε (p i)) as a product over fibers of p, i.e. as powers of sgn (ε j).

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.signCoeff {d : ℕ} (p : Fin d → Fin d) : ℝ

The “sign cancellation coefficient” associated to a map p : Fin d → Fin d.

This is the coefficient that appears when expanding the polarization sum and swapping the order of summation: it measures how many sign assignments ε survive after cancellations.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.signCoeff_eq_prod_sum_pow {d : ℕ} (p : Fin d → Fin d) : signCoeff p = ∏ j : Fin d, ∑ b : Bool, sgn b ^ (fiberCount p j + 1)

Product-of-sums form for signCoeff, expressed in terms of fiber cardinalities of p.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.signCoeff_eq_two_pow_iff_allOdd {d : ℕ} (p : Fin d → Fin d) : signCoeff p = if ∀ (j : Fin d), Odd (fiberCount p j) then 2 ^ d else 0

Evaluate signCoeff: it is 2^d iff all fibers of p have odd cardinality, and 0 otherwise.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.allOdd_fiberCount_iff_bijective {d : ℕ} (p : Fin d → Fin d) : (∀ (j : Fin d), Odd (fiberCount p j)) ↔ Function.Bijective p

For a function p : Fin d → Fin d, all fiber cardinalities are odd iff p is bijective.

Since Fin d is finite of size d, odd fibers force every fiber to have size 1.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.signCoeff_eq_two_pow_iff_bijective {d : ℕ} (p : Fin d → Fin d) : signCoeff p = if Function.Bijective p then 2 ^ d else 0

Evaluate signCoeff: it is 2^d iff p is bijective, and 0 otherwise.

Polarization identity

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.polarization_prod {d : ℕ} (u : Fin d → ℝ) : ∑ ε : Fin d → Bool, signedProd ε * signedSum ε u ^ d = 2 ^ d * ↑d.factorial * ∏ i : Fin d, u i

Polarization identity for products (algebraic form).

The signed sum of d-th powers isolates the full product ∏ i, u i, up to the constant 2^d * d!.

Compact domains: boxes and linear forms

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.boxN (n : ℕ) (M : ℝ) : Set (ReLUMlpBridge.TensorVec n)

The box [-M,M]^n as a subset of TensorVec n.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.coord_mem_Icc {n : ℕ} {M : ℝ} {x : ReLUMlpBridge.TensorVec n} (hx : x ∈ boxN n M) (i : Fin n) : ReLUMlpBridge.toVec x i ∈ Set.Icc (-M) M

A coordinate of x ∈ boxN n M lies in the interval [-M, M].

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.wPlus {n : ℕ} (i j : Fin n) : Fin n → ℝ

The weight vector e_i + e_j (sum of two standard basis vectors).

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.wMinus {n : ℕ} (i j : Fin n) : Fin n → ℝ

The weight vector e_i - e_j (difference of two standard basis vectors).

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.dot_add {n : ℕ} (w1 w2 : Fin n → ℝ) (x : ReLUMlpBridge.TensorVec n) : ReLUMlpBridge.dot (fun (k : Fin n) => w1 k + w2 k) x = ReLUMlpBridge.dot w1 x + ReLUMlpBridge.dot w2 x

Linearity of dot in the weight argument: dot (w1+w2) = dot w1 + dot w2.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.dot_neg {n : ℕ} (w : Fin n → ℝ) (x : ReLUMlpBridge.TensorVec n) : ReLUMlpBridge.dot (fun (k : Fin n) => -w k) x = -ReLUMlpBridge.dot w x

Negation compatibility for dot: dot (-w) = - dot w.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.dot_wPlus {n : ℕ} (i j : Fin n) (x : ReLUMlpBridge.TensorVec n) : ReLUMlpBridge.dot (wPlus i j) x = ReLUMlpBridge.toVec x i + ReLUMlpBridge.toVec x j

dot (e_i + e_j) x = x_i + x_j for TensorVec coordinates.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.dot_wMinus {n : ℕ} (i j : Fin n) (x : ReLUMlpBridge.TensorVec n) : ReLUMlpBridge.dot (wMinus i j) x = ReLUMlpBridge.toVec x i - ReLUMlpBridge.toVec x j

dot (e_i - e_j) x = x_i - x_j for TensorVec coordinates.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.sum_mem_Icc {n : ℕ} {M : ℝ} (_hM : 0 ≤ M) {x : ReLUMlpBridge.TensorVec n} (hx : x ∈ boxN n M) (i j : Fin n) : ReLUMlpBridge.dot (wPlus i j) x ∈ Set.Icc (-2 * M) (2 * M)

If x ∈ [-M,M]^n, then x_i + x_j ∈ [-2M, 2M].

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.diff_mem_Icc {n : ℕ} {M : ℝ} (_hM : 0 ≤ M) {x : ReLUMlpBridge.TensorVec n} (hx : x ∈ boxN n M) (i j : Fin n) : ReLUMlpBridge.dot (wMinus i j) x ∈ Set.Icc (-2 * M) (2 * M)

If x ∈ [-M,M]^n, then x_i - x_j ∈ [-2M, 2M].

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.relu_mul_coord_universal_approximation_box {n : ℕ} {M : ℝ} (hM : 0 < M) (i j : Fin n) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (l1 : Spec.LinearSpec ℝ n hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1), ∀ x ∈ boxN n M, |ReLUMlpBridge.toVec x i * ReLUMlpBridge.toVec x j - ReLUMlpBridge.mlpEvalNd l1 l2 x| < ε

Coordinate multiplication is uniformly approximable on the box [-M,M]^n.

More precisely: for fixed indices i,j : Fin n, the function x ↦ x_i * x_j can be uniformly approximated on boxN n M by a single-hidden-layer ReLU MLP.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.pow_lipschitz_Icc {R : ℝ} (hR : 0 ≤ R) (d : ℕ) (x : ℝ) : x ∈ Set.Icc (-R) R → ∀ y ∈ Set.Icc (-R) R, |x ^ d - y ^ d| ≤ ↑d * R ^ (d - 1) * |x - y|

Lipschitz bound for the power function on a bounded interval.

For x,y ∈ [-R,R], the map u ↦ u^d is Lipschitz with constant d * R^(d-1) (with the convention that the d=0 case is constant).

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.relu_universal_approximation_pow_Icc {R : ℝ} (hR : 0 < R) (d : ℕ) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (l1 : Spec.LinearSpec ℝ 1 hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1), ∀ x ∈ Set.Icc (-R) R, |x ^ d - UniversalApproximation.mlpEval1d hidDim l1 l2 x| < ε

Uniform approximation of the power function on a bounded interval by a 1D ReLU MLP.

This packages the 1D Lipschitz ReLU approximation theorem for the specific function x ↦ x^d on [-R,R].

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.linFormC {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) (w : Fin n → ℝ) : C(↑K, ℝ)

The linear form x ↦ w ⋅ x as a continuous map on the compact set K.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.linFormC_apply {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) (w : Fin n → ℝ) (x : ↑K) : (linFormC K w) x = ReLUMlpBridge.dot w ↑x

Evaluate linFormC as the dot product w ⋅ x on the underlying tensor vector.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.approx_pow_linFormC {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] (w : Fin n → ℝ) (d : ℕ) : ApproxOnC K (linFormC K w ^ d)

Uniform approximation of the continuous function x ↦ (w ⋅ x)^d on K by a 2-layer ReLU MLP.

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.wSigned {n d : ℕ} (idx : Fin d → Fin n) (ε : Fin d → Bool) : Fin n → ℝ

Weight vector encoding a signed sum of selected coordinates ∑ i, sgn(ε i) * x_{idx i}.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.dot_wSigned_eq_signedSum {n d : ℕ} (idx : Fin d → Fin n) (ε : Fin d → Bool) (x : ReLUMlpBridge.TensorVec n) : ReLUMlpBridge.dot (wSigned idx ε) x = signedSum ε fun (i : Fin d) => ReLUMlpBridge.toVec x (idx i)

dot (wSigned idx ε) x computes the signed sum of the selected coordinates of x.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.approx_coordProd_fin {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] {d : ℕ} (idx : Fin d → Fin n) : ApproxOnC K (∏ i : Fin d, UniversalApproximationND.StoneWeierstrass.coord K (idx i))

Uniform approximation of a coordinate-product monomial on a compact set.

For a fixed index map idx : Fin d → Fin n, the function x ↦ ∏ i, x_{idx i} (expressed as a product of coordinate maps on K) is uniformly approximable by a 2-layer ReLU MLP.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.approx_coordProd {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] {ι : Type} [Fintype ι] (idx : ι → Fin n) : ApproxOnC K (∏ i : ι, UniversalApproximationND.StoneWeierstrass.coord K (idx i))

Uniform approximation of a coordinate-product over an arbitrary finite index type.

This is a reindexed form of approx_coordProd_fin, using an equivalence ι ≃ Fin d.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.prod_over_multiset_eq_multiset_prod {α β : Type} [DecidableEq α] [CommMonoid β] (m : Multiset α) (f : α → β) : ∏ x : m.ToType, f x.fst = (Multiset.map f m).prod

Re-express a fintype product over a multiset as the corresponding multiset product.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.finsupp_prod_pow_eq_prod_toMultiset {α β : Type} [DecidableEq α] [CommMonoid β] (d : α →₀ ℕ) (g : α → β) : (d.prod fun (a : α) (n : ℕ) => g a ^ n) = ∏ x : (Finsupp.toMultiset d).ToType, g x.fst

Re-express a Finsupp exponent-vector product as a product over toMultiset.

This is a small bookkeeping lemma: d.prod (fun a n => (g a)^n) is the same as multiplying g a once for each occurrence of a in the multiset d.toMultiset.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.approx_aeval_coord_monomial {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] (d : Fin n →₀ ℕ) (r : ℝ) : ApproxOnC K ((MvPolynomial.aeval (UniversalApproximationND.StoneWeierstrass.coord K)) ((MvPolynomial.monomial d) r))

Uniform approximation for an evaluated coordinate monomial aeval (monomial d r) on K.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.approx_aeval_coord {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] (p : MvPolynomial (Fin n) ℝ) : ApproxOnC K ((MvPolynomial.aeval (UniversalApproximationND.StoneWeierstrass.coord K)) p)

Uniform approximation of a coordinate polynomial aeval coord p on a compact set K.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.approxOnC_of_mem_coordSubalg {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] {g : C(↑K, ℝ)} (hg : g ∈ UniversalApproximationND.StoneWeierstrass.coordSubalg K) : ApproxOnC K g

Bridge lemma: elements of the Stone–Weierstrass coordinate subalgebra are ApproxOnC-approximable.

This packages the facts that:

• coordSubalg is the range of MvPolynomial.aeval coord, and
• coordinate polynomials are approximable by ReLU MLPs (previous section).

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.relu_universal_approximation_compact {n : ℕ} (K : Set (ReLUMlpBridge.TensorVec n)) [CompactSpace ↑K] (f : C(↑K, ℝ)) : ApproxOnC K f

ReLU universal approximation on compact sets (nD).

For compact K and any continuous f : C(K,ℝ), f is uniformly approximable on K by a single-hidden-layer ReLU MLP, in the ApproxOnC sense.

Two compatibility forms for two-dimensional multiplication

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.relu_mul_universal_approximation_box2d {M : ℝ} (hM : 0 < M) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (l1 : Spec.LinearSpec ℝ 2 hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1), ∀ x ∈ ReLUMulApprox.box M, |ReLUMulApprox.mulFun x - ReLUMlpBridge.mlpEvalNd l1 l2 x| < ε

Compatibility theorem for the standalone 2D multiplication construction from ReLUMulApprox.

The n-dimensional development below subsumes this result, but keeping this theorem name gives downstream files a stable import point for the classical two-coordinate multiplication statement.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.boxN_two_iff_box (M : ℝ) (x : ReLUMulApprox.TensorVec2) : x ∈ boxN 2 M ↔ x ∈ ReLUMulApprox.box M

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.relu_mul_universal_approximation_box2d_via_nd {M : ℝ} (hM : 0 < M) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (l1 : Spec.LinearSpec ℝ 2 hidDim) (l2 : Spec.LinearSpec ℝ hidDim 1), ∀ x ∈ ReLUMulApprox.box M, |ReLUMulApprox.mulFun x - ReLUMlpBridge.mlpEvalNd l1 l2 x| < ε

The same 2D multiplication guarantee derived from the nD coordinate-product theorem.

This theorem is a cross-check between the specialized two-dimensional construction and the general coordinate-product approximation pipeline used by the compact-set theorem.