Documentation

CompPoly.Univariate.NTT.Evaluation

NTT and Evaluation #

Bridge definitions and theorems connecting the NTT specification layer to evaluation on the root-of-unity domain.

source
def CompPoly.CPolynomial.NTT.evalOnDomain {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) :
Array R

Evaluate a raw polynomial on all nodes of an NTT domain in natural order.

Instances For
    source
    theorem CompPoly.CPolynomial.NTT.evalOnDomain_eq_evalBatch {R : Type u_1} [Field R] (D : Domain R) (p : CPolynomial R) :
    evalOnDomain D ↑p = p.evalBatch (Array.ofFn fun (k : D.Idx) => D.node k)

    evalOnDomain is evalBatch specialized to the NTT domain nodes.

    source
    theorem CompPoly.CPolynomial.NTT.Forward.forwardSpec_eval_node_eq {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) (hdeg : p.toPoly.natDegree < D.n) (k : D.Idx) :
    (forwardSpec D p)[↑k] = Raw.eval (D.node k) p

    Pointwise form: the forward NTT specification evaluates a raw polynomial at a domain node.

    source
    theorem CompPoly.CPolynomial.NTT.Forward.forwardSpec_eq_evalOnDomain {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) (hdeg : p.toPoly.natDegree < D.n) :
    forwardSpec D p = evalOnDomain D p

    The forward NTT specification evaluates a raw polynomial on all domain nodes.

    source
    theorem CompPoly.CPolynomial.NTT.Forward.forwardImpl_eval_node_eq {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) (hdeg : p.toPoly.natDegree < D.n) (k : D.Idx) :
    (forwardImpl D p).getD (↑k) 0 = Raw.eval (D.node k) p

    Pointwise form: the forward NTT implementation evaluates a raw polynomial at a domain node.

    source
    theorem CompPoly.CPolynomial.NTT.Forward.forwardImpl_eq_evalOnDomain {R : Type u_1} [Field R] (D : Domain R) (p : Raw R) (hdeg : p.toPoly.natDegree < D.n) :
    forwardImpl D p = evalOnDomain D p

    The forward NTT implementation evaluates a raw polynomial on all domain nodes.