Email Gateway (Sep 07 2022 at 11:12): Email Gateway (Sep 07 2022 at 11:12):From: Manuel Eberl <manuel@pruvisto.org>
Number Theoretic Transform
by Thomas Ammer and Katharina Kreuzer
This entry contains an Isabelle formalization of the Number Theoretic
Transform (NTT) which is the analogue to a Discrete Fourier Transform
(DFT) over a finite field. Roots of unity in the complex numbers are
replaced by those in a finite field.
First, we define both NTT and the inverse transform INTT in Isabelle and
prove them to be mutually inverse.
DFT can be efficiently computed by the recursive Fast Fourier Transform
(FFT). In our formalization, this algorithm is adapted to the setting of
the NTT: We implement a Fast Number Theoretic Transform (FNTT) based on
the Butterfly scheme by Cooley and Tukey. Additionally, we provide an
inverse transform IFNTT and prove it mutually inverse to FNTT.
Afterwards, a recursive formalization of the FNTT running time is
examined and the famous
bounds O(n log n) are proven.
https://www.isa-afp.org/entries/Number_Theoretic_Transform.html
Enjoy
Manuel
Last updated: Apr 25 2024 at 12:23 UTC