def Hex.ZMod64.Ntt.evalCoeffs {p : Nat} [Bounds p] (x : ZMod64 p) : List (ZMod64 p) → ZMod64 p

Evaluate a low-to-high coefficient list by Horner recursion.

Equations

• Hex.ZMod64.Ntt.evalCoeffs x [] = 0
• Hex.ZMod64.Ntt.evalCoeffs x (value :: values) = value + x * Hex.ZMod64.Ntt.evalCoeffs x values

@[simp]

theorem Hex.ZMod64.Ntt.evalCoeffs_nil {p : Nat} [Bounds p] (x : ZMod64 p) : evalCoeffs x [] = 0

Evaluation of an empty coefficient list is zero.

@[simp]

theorem Hex.ZMod64.Ntt.evalCoeffs_cons {p : Nat} [Bounds p] (x value : ZMod64 p) (values : List (ZMod64 p)) : evalCoeffs x (value :: values) = value + x * evalCoeffs x values

Horner equation for a nonempty coefficient list.

def Hex.ZMod64.Ntt.dftCoeff {p : Nat} [Bounds p] (root : ZMod64 p) (values : List (ZMod64 p)) (k : Nat) : ZMod64 p

The coefficientwise DFT value at frequency k.

Equations

• Hex.ZMod64.Ntt.dftCoeff root values k = Hex.ZMod64.Ntt.evalCoeffs (root ^ k) values

@[simp]

theorem Hex.ZMod64.Ntt.dftCoeff_eq {p : Nat} [Bounds p] (root : ZMod64 p) (values : List (ZMod64 p)) (k : Nat) : dftCoeff root values k = evalCoeffs (root ^ k) values

Expose a DFT coefficient as evaluation at the corresponding root power.

def Hex.ZMod64.Ntt.dft {p : Nat} [Bounds p] (root : ZMod64 p) (count : Nat) (values : List (ZMod64 p)) : List (ZMod64 p)

The first count coefficientwise DFT values in ordinary frequency order.

Equations

• Hex.ZMod64.Ntt.dft root count values = List.ofFn fun (k : Fin count) => Hex.ZMod64.Ntt.dftCoeff root values ↑k

def Hex.ZMod64.Ntt.dftArray {p : Nat} [Bounds p] (root : ZMod64 p) (count : Nat) (values : Array (ZMod64 p)) : Array (ZMod64 p)

Array wrapper around the coefficientwise DFT reference.

Equations

• Hex.ZMod64.Ntt.dftArray root count values = (Hex.ZMod64.Ntt.dft root count values.toList).toArray

@[simp]

theorem Hex.ZMod64.Ntt.length_dft {p : Nat} [Bounds p] (root : ZMod64 p) (count : Nat) (values : List (ZMod64 p)) : (dft root count values).length = count

A coefficientwise DFT has its requested output length.

@[simp]

theorem Hex.ZMod64.Ntt.size_dftArray {p : Nat} [Bounds p] (root : ZMod64 p) (count : Nat) (values : Array (ZMod64 p)) : (dftArray root count values).size = count

A coefficientwise DFT array has its requested output size.

@[simp]

theorem Hex.ZMod64.Ntt.getElem_dft {p : Nat} [Bounds p] (root : ZMod64 p) (count : Nat) (values : List (ZMod64 p)) (k : Nat) (hk : k < count) : (dft root count values)[k] = dftCoeff root values k

Lookup exposes the defining coefficient-evaluation formula.

@[simp]

theorem Hex.ZMod64.Ntt.dft_one {p : Nat} [Bounds p] (root value : ZMod64 p) : dft root 1 [value] = [value]

The one-point DFT of a singleton is that singleton.

theorem Hex.ZMod64.Ntt.evalCoeffs_append {p : Nat} [Bounds p] (x : ZMod64 p) (left right : List (ZMod64 p)) : evalCoeffs x (left ++ right) = evalCoeffs x left + x ^ left.length * evalCoeffs x right

Evaluation of concatenated coefficient blocks shifts the right block by the length of the left block.

theorem Hex.ZMod64.Ntt.evalCoeffs_append_eq_add {p : Nat} [Bounds p] (x : ZMod64 p) (left right : List (ZMod64 p)) (hpow : x ^ left.length = 1) : evalCoeffs x (left ++ right) = evalCoeffs x left + evalCoeffs x right

When the block-shift power is one, concatenated evaluation is the sum of the two block evaluations.

theorem Hex.ZMod64.Ntt.evalCoeffs_append_eq_sub {p : Nat} [Bounds p] (x : ZMod64 p) (left right : List (ZMod64 p)) (hpow : x ^ left.length = 0 - 1) : evalCoeffs x (left ++ right) = evalCoeffs x left - evalCoeffs x right

When the block-shift power is minus one, concatenated evaluation is the difference of the two block evaluations.

theorem Hex.ZMod64.Ntt.evalCoeffs_scale {p : Nat} [Bounds p] (x c : ZMod64 p) (values : List (ZMod64 p)) : evalCoeffs x (List.map (fun (value : ZMod64 p) => c * value) values) = c * evalCoeffs x values

Evaluation commutes with multiplication of every coefficient by a common scalar.

theorem Hex.ZMod64.Ntt.pow_mul {p : Nat} [Bounds p] (x : ZMod64 p) (a b : Nat) : (x ^ a) ^ b = x ^ (a * b)

Raising a power and then raising again multiplies the exponents.

theorem Hex.ZMod64.Ntt.negOne_pow_even {p : Nat} [Bounds p] (k : Nat) : (0 - 1) ^ (2 * k) = 1

Even powers of minus one are one.

theorem Hex.ZMod64.Ntt.negOne_pow_odd {p : Nat} [Bounds p] (k : Nat) : (0 - 1) ^ (2 * k + 1) = 0 - 1

Odd powers of minus one are minus one.

theorem Hex.ZMod64.Ntt.pow_mod {p n : Nat} [Bounds p] (root : ZMod64 p) (hroot : root ^ n = 1) (e : Nat) : root ^ (e % n) = root ^ e

A root whose nth power is one has periodic powers modulo positive n.