Subproduct-Tree Batch Evaluation

Executable subproduct-tree construction and descent for univariate batch evaluation.

inductive CompPoly.CPolynomial.SubproductTree (R : Type u_2) [Zero R] : Type u_2

A subproduct tree stores the product polynomial at every node.

• leaf {R : Type u_2} [Zero R] (x : R) (poly : CPolynomial R) : SubproductTree R

  A leaf for one evaluation point. The polynomial is X - C x.

• node {R : Type u_2} [Zero R] (poly : CPolynomial R) (left right : SubproductTree R) : SubproductTree R

  An internal node stores the product of its children.

def CompPoly.CPolynomial.SubproductTree.poly {R : Type u_1} [Zero R] : SubproductTree R → CPolynomial R

The product polynomial stored at the root of a subproduct tree.

def CompPoly.CPolynomial.SubproductTree.leafFor {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (x : R) : SubproductTree R

Build a leaf for one evaluation point.

def CompPoly.CPolynomial.SubproductTree.combine {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (left right : SubproductTree R) : SubproductTree R

Combine two neighboring trees using the selected multiplication backend.

def CompPoly.CPolynomial.SubproductTree.combinePairs {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) : List (SubproductTree R) → List (SubproductTree R)

Pair adjacent trees into the next subproduct-tree level.

def CompPoly.CPolynomial.SubproductTree.buildFromTrees {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) : ℕ → List (SubproductTree R) → Option (SubproductTree R)

Repeatedly combine tree levels, bounded by fuel for straightforward termination.

def CompPoly.CPolynomial.SubproductTree.buildList {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (xs : List R) : Option (SubproductTree R)

Build a subproduct tree from an ordered list of evaluation points.

def CompPoly.CPolynomial.SubproductTree.buildArray {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (xs : Array R) : Option (SubproductTree R)

Build a subproduct tree from an ordered array of evaluation points.

def CompPoly.CPolynomial.SubproductTree.evalList {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : ModContext R) (p : CPolynomial R) : SubproductTree R → List R

Descend a subproduct tree with remainders and return values in leaf order.

def CompPoly.CPolynomial.evalBatchSubproduct {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (D : ModContext R) (p : CPolynomial R) (xs : Array R) : Array R

Evaluate a polynomial at many points using a subproduct tree.