Waring terms

A term is a scaled d-th power of a homogeneous linear form in d variables. Its coefficients can be interpreted in another semiring, including the formal polynomial semiring. This module is shared by the arithmetic compiler and the term-count lower bounds.

Main definitions

• Cslib.Circuits.Waring.Term: a scale and a finite family of coefficient symbols.
• Cslib.Circuits.Waring.Term.eval: interpret the symbols and evaluate at an input.
• Cslib.Circuits.Waring.Term.polynomial: the represented formal polynomial.

References

• Adapted from LowerBound/Fusion/SumOfTerms/Waring.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

structure Cslib.Circuits.Waring.Term (K : Type u_1) (d : ℕ) : Type u_1

A scalar multiple of a d-th power of a homogeneous linear form in d variables.

• scale : K

  The scalar multiplying the power.

• coefficients : Fin d → K

  Coefficients of the homogeneous linear form.

def Cslib.Circuits.Waring.Term.eval {C : Type u_1} {R : Type u_2} [Semiring R] {d : ℕ} (t : Term C d) (constant : C → R) (x : Fin d → R) : R

Interpret the coefficient symbols and evaluate the scaled power.

noncomputable def Cslib.Circuits.Waring.Term.polynomial {K : Type u_1} [CommSemiring K] {d : ℕ} (t : Term K d) : MvPolynomial (Fin d) K

The polynomial represented by a Waring dictionary term.