Among all N-level quantizers on [a,b], the log-uniform quantizer uniquely minimizes worst-case NMSE (and MSRE) over all densities. The minimax value is ε²/12 + O(ε⁴) = (R·ln2)²/(12N²). For B=8 bits, R=16 octaves: NMSE* = 1.564×10⁻⁴ (SQNR = 38.1 dB). Verified in Lean 4.
This theorem is the central theoretical result of the QF8 paper. It proves that the log-uniform quantizer — the quantizer where consecutive representable values have a constant ratio — is the unique best choice when you want to minimize the worst-case NMSE (normalized mean squared error, the fraction of signal power lost to quantization) regardless of what distribution the input values follow.
This matters for ML because weight, activation, and gradient distributions vary widely across layers and training stages. A format that is optimal only for Gaussian inputs might fail on heavy-tailed gradients. Log-uniform quantization sidesteps this: it delivers the same NMSE for any input distribution.
Among all N-level quantizers on [a,b], the log-uniform quantizer uniquely minimizes the worst-case NMSE (and MSRE) over all densities:
The minimax value is:
where ε = R·ln2/N is the bin width in the log domain, R is the dynamic range in octaves, and N is the number of quantization levels.
For B = 8 bits (N = 256), R = 16 octaves: NMSE = 1.564 × 10⁻⁴* (SQNR = 38.1 dB).
Step 1 (Density-independence / Equalization property). For the log-uniform quantizer, the cell width at any point x is proportional to x itself: w(x) ≈ x·ε. Under the high-resolution approximation:
The x² factors cancel exactly — the density f drops out completely. This is the equalization property: the log-uniform quantizer achieves the same NMSE regardless of input distribution.
Numerically verified for three test densities (log-uniform, uniform, f ∝ x²) with N=256, R=16: all give NMSE = 1.564 × 10⁻⁴ within < 0.1% deviation.
Step 2 (Non-constant φ is worse for some density). Define φ(x) = w(x)/x (relative cell width). For any non-log-uniform quantizer, φ is not constant — it must be larger somewhere and smaller elsewhere. Let x* = argmax φ(x). An adversary can concentrate the input density near x* to exploit the wider cells there, achieving MSRE > ε²/12.
Step 3 (Uniqueness). If Q ≠ Q_log, then φ is non-constant and Step 2 gives strict inequality. The log-uniform quantizer is the unique minimax optimizer.
The same quantizer also minimizes worst-case MSRE (mean squared relative error). The proof is identical.
Lean 4 verified (see attached proofs/MinimaxNMSE.lean): constant relative error across all bins for N=16, range [1, 256]. Perturbation tests confirm any deviation from log-uniform spacing increases the maximum error.