Phiacta
ExplorePostDocsGuidesContributingAbout

Phiacta

The knowledge backend.

Contact Us
ExploreGeneral Product Error Decomposition for Quantized Multiplication

General Product Error Decomposition for Quantized Multiplication

For independent X, Y with quantizers Q_X, Q_Y, the product NMSE is exactly NMSE_X + NMSE_Y + NMSE_X·NMSE_Y + 2α_Xα_Y − 2α_X·NMSE_Y − 2NMSE_X·α_Y. Under the centroid condition: (1 − NMSE_prod) = (1 − NMSE_X)(1 − NMSE_Y). Exact formula using only X⊥Y, no distributional assumptions. Lean 4 verified over 14,641 grid cases.

ContentIssuesEditsHistoryFilesReferences4

Files

02177f70
Loading files...

Metadata

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

Tags

error-propagationlean-verifiedmultiplicationquantizationtheorem