Vanishing Polynomials for Array Nodes

Reusable executable construction of ∏ x in xs, (X - x).

def CompPoly.CPolynomial.vanishingPolynomialArray {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (xs : Array F) : CPolynomial F

Direct folded vanishing polynomial ∏ x in xs, (X - x).

structure CompPoly.CPolynomial.VanishingPolynomialContext (F : Type u_2) [Field F] [BEq F] [LawfulBEq F] : Type u_2

Operation dictionary for array vanishing-polynomial construction.

• vanishingPolynomial : Array F → CPolynomial F
• correct (xs : Array F) : self.vanishingPolynomial xs = vanishingPolynomialArray xs

def CompPoly.CPolynomial.VanishingPolynomialContext.direct {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] : VanishingPolynomialContext F

Direct folded vanishing-polynomial context.

def CompPoly.CPolynomial.VanishingPolynomialContext.subproduct {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : MulContext F) : VanishingPolynomialContext F

Subproduct-tree-backed vanishing-polynomial context.

theorem CompPoly.CPolynomial.eval_vanishingPolynomialArray_eq_zero_of_mem {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (xs : Array F) {x : F} (hx : x ∈ xs.toList) : eval x (vanishingPolynomialArray xs) = 0

Every listed node is a root of the direct vanishing polynomial.