Documentation

CompPoly.Univariate.NTT.Inverse

Inverse NTT #

This file provides inverse NTT APIs and correctness statement.

source
def CompPoly.CPolynomial.NTT.Inverse.inttAt {R : Type u_1} [Field R] (D : Domain R) (v : Array R) (k : D.Idx) :
R

Inverse NTT formula at one output index.

Instances For
    source
    def CompPoly.CPolynomial.NTT.Inverse.inverseSpec {R : Type u_1} [Field R] (D : Domain R) (v : Array R) :
    Array R

    Full inverse transform on arrays, specified from inttAt.

    Instances For
      source
      def CompPoly.CPolynomial.NTT.Inverse.normalize {R : Type u_1} [Field R] (D : Domain R) (a : Array R) :
      Array R

      Apply the final n⁻¹ normalization for the inverse transform.

      Instances For
        source
        @[simp]
        theorem CompPoly.CPolynomial.NTT.Inverse.size_inverseSpec {R : Type u_1} [Field R] (D : Domain R) (v : Array R) :
        (inverseSpec D v).size = D.n
        source
        @[simp]
        theorem CompPoly.CPolynomial.NTT.Inverse.size_normalize {R : Type u_1} [Field R] (D : Domain R) (a : Array R) :
        (normalize D a).size = D.n
        source
        theorem CompPoly.CPolynomial.NTT.Inverse.normalize_forwardSpec_inverse_eq_inverseSpec {R : Type u_1} [Field R] (D : Domain R) (v : Array R) :
        normalize D (Forward.forwardSpec D.inverse v) = inverseSpec D v
        source
        def CompPoly.CPolynomial.NTT.Inverse.inverseImpl {R : Type u_1} [Field R] (D : Domain R) (v : Array R) :
        Raw R

        Intended fast implementation entry point for inverse NTT.

        Instances For
          source
          theorem CompPoly.CPolynomial.NTT.Inverse.inverseImpl_correct {R : Type u_1} [Field R] (D : Domain R) (v : Array R) :
          inverseImpl D v = inverseSpec D v