hex

6.4. Conversions🔗

The dense conversions are the boundary between the two representations and the proof route for the multiplicative laws. toDense is the one operation whose cost is governed by the degree.

🔗def
Hex.SparsePoly.toDense.{u} {R : Type u} [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) : Hex.DensePoly R
Hex.SparsePoly.toDense.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) : Hex.DensePoly R

Convert to the dense representation: allocate degree + 1 coefficients and write each stored term into its slot, O(n) in the degree whatever the term count. The one operation here whose cost is not governed by the term count; no operation in this library is implemented through it.

🔗def
Hex.SparsePoly.ofDense.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Hex.SparsePoly R
Hex.SparsePoly.ofDense.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Hex.SparsePoly R

Convert from the dense representation, keeping the nonzero coefficients with their indices.

Kernel-facing specification (an ordered List walk); compiled code uses Hex.SparsePoly.ofDenseImpl, the value-equal array pass selected by Hex.SparsePoly.ofDense_eq_impl.

🔗theorem
Hex.SparsePoly.toDense_mul.{u} {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] (s t : Hex.SparsePoly S) :
  (s * t).toDense = s.toDense * t.toDense
Hex.SparsePoly.toDense_mul.{u}
  {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S]
  (s t : Hex.SparsePoly S) :
  (s * t).toDense = s.toDense * t.toDense

The conversion is multiplicative: the transported convolution. This is where coeff_mul and the multiplicative ring laws come from.

Measured crossovers (recorded in the library SPEC): sparse addition beats dense up to about t ≈ n/8 stored terms at degree n, sparse multiplication up to about t ≈ n/4, and sparse evaluation stays ahead to at least t ≈ n/6.