ReLU approximation on compact sets (nD)

Key theorems proved in this file:

• polarization_prod: the signed sum of d-th powers over {±1}^d isolates a product of d reals, which reduces coordinate monomials to ridge functions of linear forms.
• relu_mul_coord_universal_approximation_box: the coordinate product x_i * x_j is uniformly approximable on the box [-M, M]^n.
• 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.StoneWeierstrass (Stone–Weierstrass density of coordinate polynomials on compact sets of tensor vectors).
• NN.MLTheory.Proofs.ReLU.Bridge.ReLUMlpBridge (lifting 1D MLP constructions to Tensor ℝ [n]).

Network algebra shared by the closure properties

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.mlpEval_append_add {n m k : ℕ} (l1f : Spec.LinearSpec ℝ n m) (l1g : Spec.LinearSpec ℝ n k) (l2f : Spec.LinearSpec ℝ m 1) (l2g : Spec.LinearSpec ℝ k 1) (x : TorchLean.Tensor ℝ [n]) : ReLUMlpBridge.mlpEval (ReLUMulApprox.appendLinearSpec l1f l1g) (ReLUMulApprox.combineOutput 1 1 0 l2f l2g) x = ReLUMlpBridge.mlpEval l1f l2f x + ReLUMlpBridge.mlpEval l1g l2g x

Appending the hidden layers of two networks and adding their scalar outputs evaluates to the sum of the two networks.

noncomputable def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.scaleOutput {m : ℕ} (c : ℝ) (l2 : Spec.LinearSpec ℝ m 1) : Spec.LinearSpec ℝ m 1

Scale the weights and bias of a scalar output layer by c.

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.mlpEval_scaleOutput {n m : ℕ} (c : ℝ) (l1 : Spec.LinearSpec ℝ n m) (l2 : Spec.LinearSpec ℝ m 1) (x : TorchLean.Tensor ℝ [n]) : ReLUMlpBridge.mlpEval l1 (scaleOutput c l2) x = c * ReLUMlpBridge.mlpEval l1 l2 x

The network output is affine in the output layer, so scaling that layer scales the output.

Uniform approximation of continuous maps on K

The predicate is stated for C(K, ℝ) so that Stone–Weierstrass applies directly.

def NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC {n : ℕ} (K : Set (TorchLean.Tensor ℝ [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 (mlpEval, evaluated on the underlying point x.1).

Closure properties

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.ApproxOnC.zero {n : ℕ} (K : Set (TorchLean.Tensor ℝ [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 (TorchLean.Tensor ℝ [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 (TorchLean.Tensor ℝ [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 (TorchLean.Tensor ℝ [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 (TorchLean.Tensor ℝ [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 (TorchLean.Tensor ℝ [n])) : UniversalApproximation.StoneWeierstrass.coordSubalg K = (MvPolynomial.aeval (UniversalApproximation.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 (TorchLean.Tensor ℝ [n])

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

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, |x.getScalar i * x.getScalar j - ReLUMlpBridge.mlpEval 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.mlpEvalScalar 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 (TorchLean.Tensor ℝ [n])) (w : Fin n → ℝ) : C(↑K, ℝ)

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

theorem NN.MLTheory.Proofs.ReLU.Approximation.CompactSet.linFormC_apply {n : ℕ} (K : Set (TorchLean.Tensor ℝ [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 (TorchLean.Tensor ℝ [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, by ridge-lifting the 1D power approximation.

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 : TorchLean.Tensor ℝ [n]) : ReLUMlpBridge.dot (wSigned idx ε) x = signedSum ε fun (i : Fin d) => x.getScalar (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 (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] {d : ℕ} (idx : Fin d → Fin n) : ApproxOnC K (∏ i : Fin d, UniversalApproximation.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 (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] {ι : Type} [Fintype ι] (idx : ι → Fin n) : ApproxOnC K (∏ i : ι, UniversalApproximation.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 (coerced to a type) as the corresponding multiset product of m.map f.

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 (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] (d : Fin n →₀ ℕ) (r : ℝ) : ApproxOnC K ((MvPolynomial.aeval (UniversalApproximation.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 (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] (p : MvPolynomial (Fin n) ℝ) : ApproxOnC K ((MvPolynomial.aeval (UniversalApproximation.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 (TorchLean.Tensor ℝ [n])) [CompactSpace ↑K] {g : C(↑K, ℝ)} (hg : g ∈ UniversalApproximation.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 (TorchLean.Tensor ℝ [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.