NTT Kernel Identities

Shared root-of-unity orthogonality lemmas used by NTT evaluation, interpolation, and multiplication proofs.

theorem CompPoly.CPolynomial.NTT.omegaInv_pow_mul_eq {R : Type u_1} [Field R] (D : Domain R) {i : ℕ} (hi : i < D.n) (k : ℕ) : D.omegaInv ^ (i * k) = D.omega ^ ((D.n - i) * k)

Rewrite powers of the inverse root as powers of the forward root.

theorem CompPoly.CPolynomial.NTT.kernel_term_eq {R : Type u_1} [Field R] (D : Domain R) {i : ℕ} (hi : i < D.n) (j k : ℕ) : D.omega ^ (k * j) * D.omegaInv ^ (i * k) = D.omega ^ ((j + (D.n - i)) * k)

Combine a forward-kernel term with an inverse-kernel term.

theorem CompPoly.CPolynomial.NTT.omega_sum_pow_mul_eq_if_dvd {R : Type u_1} [Field R] (D : Domain R) (m : ℕ) : ∑ k : D.Idx, D.omega ^ (m * ↑k) = if D.n ∣ m then ↑D.n else 0

Sum of powers over the NTT domain, expressed by divisibility of the exponent.

theorem CompPoly.CPolynomial.NTT.dvd_add_sub_iff_fin_eq {R : Type u_1} [Field R] (D : Domain R) (i j : D.Idx) : D.n ∣ ↑j + (D.n - ↑i) ↔ j = i

The kernel divisibility condition is equivalent to equality of domain indices.

theorem CompPoly.CPolynomial.NTT.kernel_sum_eq_if {R : Type u_1} [Field R] (D : Domain R) (i j : D.Idx) : ∑ k : D.Idx, D.omega ^ (↑k * ↑j) * D.omegaInv ^ (↑i * ↑k) = if j = i then ↑D.n else 0

Orthogonality of the forward/inverse NTT kernels over the domain.

theorem CompPoly.CPolynomial.NTT.kernel_sum_forward_inverse_eq_if {R : Type u_1} [Field R] (D : Domain R) (i j : D.Idx) : ∑ k : D.Idx, D.omegaInv ^ (↑k * ↑j) * D.omega ^ (↑i * ↑k) = if j = i then ↑D.n else 0

Orthogonality of the inverse/forward NTT kernels over the domain.