hex

6.5. Evaluation and substitution🔗

Evaluation is gap Horner: one pass over the stored terms with binary powering across exponent gaps, O(t) coefficient multiplications plus O(t log (n/t)) squarings.

🔗def
Hex.SparsePoly.eval.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  [Mul R] (s : Hex.SparsePoly R) (x : R) : R
Hex.SparsePoly.eval.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (s : Hex.SparsePoly R) (x : R) : R

Evaluate at x by Horner over the exponent gaps: writing m for the term count and n for the degree, m additions and O(m · log(n/m + 1)) multiplications, against DensePoly's O(n).

🔗def
Hex.SparsePoly.derivative.{u} {R : Type u} [Zero R] [DecidableEq R]
  [NatCast R] [Mul R] (s : Hex.SparsePoly R) : Hex.SparsePoly R
Hex.SparsePoly.derivative.{u} {R : Type u}
  [Zero R] [DecidableEq R] [NatCast R]
  [Mul R] (s : Hex.SparsePoly R) :
  Hex.SparsePoly R

The formal derivative: c · x^e maps to (e : R) · c · x^(e−1), the e = 0 term is dropped, and — the invariant hazard — a coefficient (e : R) * c that vanishes (every exponent divisible by p over ZMod64 p) drops its term rather than storing a zero.

🔗def
Hex.SparsePoly.substPow.{u} {R : Type u} [Zero R] [DecidableEq R]
  [Add R] (s : Hex.SparsePoly R) (k : ℕ) : Hex.SparsePoly R
Hex.SparsePoly.substPow.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R]
  (s : Hex.SparsePoly R) (k : ℕ) :
  Hex.SparsePoly R

Substitute x^k for x: multiply every exponent by k. For k ≥ 1 the map is strictly monotone, so the terms, their order, and their coefficients are unchanged and the cost is O(t). For k = 0 every term lands on exponent 0, so the result is the combined constant, which can vanish; that case is a canonicalisation to perform, not an input to reject.

🔗def
Hex.SparsePoly.substScale.{u} {R : Type u} [Zero R] [DecidableEq R]
  [Mul R] (s : Hex.SparsePoly R) (a : R) : Hex.SparsePoly R
Hex.SparsePoly.substScale.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Mul R]
  (s : Hex.SparsePoly R) (a : R) :
  Hex.SparsePoly R

Scale the argument: c · x^e maps to (c · a^e) · x^e, with the powers of a computed from the exponent gaps as eval computes its powers of x. Exponents are unchanged; coefficients can vanish when a is a zero divisor or zero, so the zero filter applies.

🔗def
Hex.SparsePoly.compose.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  [Mul R] (s t : Hex.SparsePoly R) : Hex.SparsePoly R
Hex.SparsePoly.compose.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R

Substitute t for the variable of s: one fold of composeStep over the terms, carrying the running power of t across each exponent gap.