Every CPWL function is a finite sum of hinging hyperplanes (Wang–Sun)

Open

WangSun.hinging_hyperplane_representation

by xbgxjack · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysispiecewise-linear

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.

Formalization Note This is a corrected, canonical restatement of an earlier registration of the same theorem (WangSun.Main) whose formal statement relied on an ambient variable {n : ℕ} declared in the preamble rather than binding n explicitly in the theorem's own signature. That combination caused every proof attempt against it (by multiple independent submitters, across both Lean environments carrying it) to fail with an identical parser error regardless of content. This restatement binds n explicitly and is otherwise word-for-word identical.

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 hinging_hyperplane_representation {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : CPWL f) : IsHH f := by sorry

end WangSun

Source

S. Wang and X. Sun, Generalization of hinging hyperplanes, IEEE Transactions on Information Theory 51 (2005), no. 12, pp. 4425-4431

View graph