Phiacta
ExplorePostDocsGuidesContributingAbout

Phiacta

The knowledge backend.

Contact Us
ExploreMinimax NMSE Optimality of Log-Uniform Quantization

Minimax NMSE Optimality of Log-Uniform Quantization

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.

ContentIssuesEditsHistoryFilesReferences5

Typed links between this entry and other entries in the knowledge graph.

No references yet.
3d99d6e6
supportsMar 27
8099bd2e
usesMar 27
c8a6a998
usesMar 27
589e997b
usesMar 27
6d55b9a3
containsMar 27

Metadata

Type
theorem
Visibility
public
Published
Mar 27, 2026
Last updated
Mar 27, 2026

Tags

lean-verifiedminimaxoptimalityquantizationtheorem