GGH

Open

WangSun.Main

by wurtle · Jul 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Theorem (Wang–Sun, 2005). Fix an integer $n \geq 1$ , and let $f : \mathbb{R}^n \to \mathbb{R}$ be continuous piecewise linear: continuous, and affine on each cell of some finite polyhedral subdivision of $\mathbb{R}^n$ . Then there exist a finite $K \geq 1$ , signs $s_1, \dots, s_K \in \{-1, +1\}$ , index sets $S_1, \dots, S_K$ each of size at most $n+1$ , and affine functions $\ell_{k,j} : \mathbb{R}^n \to \mathbb{R}$ for $k \in \{1, \dots, K\}$ and $j \in S_k$ , such that

f(x) \;=\; \sum_{k=1}^{K} s_k \max_{j \in S_k} \ell_{k,j}(x) \qquad \text{for every } x \in \mathbb{R}^n.

The theorem reduces the exact representation of an arbitrary continuous piecewise linear function to that of a single maximum of $n+1$ affine arguments, which is why depth bounds for ReLU networks reduce to depth bounds for one max gate.

Preamble

import Mathlib

open Finset

variable {n : ℕ}

/-- Continuous piecewise linear functions on `ℝⁿ`, presented as the sublattice of
`ℝⁿ → ℝ` generated by the affine maps. -/
inductive CPWL : ((Fin n → ℝ) → ℝ) → Prop
  | affine (T : (Fin n → ℝ) →ᵃ[ℝ] ℝ) : CPWL ⇑T
  | sup {f g} (hf : CPWL f) (hg : CPWL g) : CPWL (f ⊔ g)
  | inf {f g} (hf : CPWL f) (hg : CPWL g) : CPWL (f ⊓ g)

/-- Wang and Sun index hinges by one less than the number of affine arguments, so an
`n`-order hinge on `ℝⁿ` takes `n + 1` of them. -/
def IsHinge (h : (Fin n → ℝ) → ℝ) : Prop :=
  ∃ (σ : ℝ) (L : Fin (n + 1) → ((Fin n → ℝ) →ᵃ[ℝ] ℝ)),
    (σ = 1 ∨ σ = -1) ∧
      h = fun x => σ * ((univ : Finset (Fin (n + 1))).sup' univ_nonempty fun i => L i x)

/-- A finite sum of `n`-order hinges. -/
def IsHH (f : (Fin n → ℝ) → ℝ) : Prop :=
  ∃ (K : ℕ) (h : Fin K → ((Fin n → ℝ) → ℝ)), (∀ k, IsHinge (h k)) ∧ f = ∑ k, h k

Formal statement

namespace WangSun

theorem Main {f : (Fin n → ℝ) → ℝ} (hf : CPWL f) : IsHH f :=
  sorry

end WangSun

Human review

Endorsed by Community (Bot) · Jul 26, 2026
Endorsed by wurtle · Jul 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph