Substituting a source polynomial into an interpolating family #
For each base-h monomial, substitute the powers of the source polynomial
reduced modulo E, then multiply by its coefficient polynomial. The sum is
an ordinary polynomial in the seed variable. It is the witness to which the
first root-count argument in the GUV expansion proof applies.
noncomputable def
Algebraic.Cutwidth.Extractor.substitutedSum
{F : Type u_1}
[CommRing F]
{K : ℕ}
(E : Polynomial F)
(h m : ℕ)
(p : Fin K → Polynomial F)
(f : Polynomial F)
:
Substitute the reduced source powers into all K interpolation monomials.
Equations
- Algebraic.Cutwidth.Extractor.substitutedSum E h m p f = ∑ j : Fin K, p j * Algebraic.Cutwidth.Extractor.digitMonomial h ↑j fun (i : Fin m) => f ^ h ^ ↑i %ₘ E