def Hex.SparsePoly.termsBound {R : Type u} (ts : Array (Nat × R)) : Nat

One more than the largest exponent of a term array (0 when empty): the number of coefficients its dense form stores.

Equations

• Hex.SparsePoly.termsBound ts = Array.foldl (fun (m : Nat) (t : Nat × R) => max m (t.fst + 1)) 0 ts

theorem Hex.SparsePoly.le_foldl_max {R : Type u} (l : List (Nat × R)) (init : Nat) : init ≤ List.foldl (fun (m : Nat) (t : Nat × R) => max m (t.fst + 1)) init l

The bound fold dominates its initial value.

theorem Hex.SparsePoly.exp_lt_foldl_max {R : Type u} {l : List (Nat × R)} {t : Nat × R} (ht : t ∈ l) (init : Nat) : t.fst < List.foldl (fun (m : Nat) (t : Nat × R) => max m (t.fst + 1)) init l

Every stored exponent is below the bound.

theorem Hex.SparsePoly.foldl_max_le {R : Type u} {l : List (Nat × R)} {n : Nat} (init : Nat) (h0 : init ≤ n) (h : ∀ (t : Nat × R), t ∈ l → t.fst < n) : List.foldl (fun (m : Nat) (t : Nat × R) => max m (t.fst + 1)) init l ≤ n

The bound is least among exponent bounds at or above its initial value.

theorem Hex.SparsePoly.size_foldl_set {R : Type u} (l : List (Nat × R)) (base : Array R) : (List.foldl (fun (acc : Array R) (t : Nat × R) => acc.setIfInBounds t.fst t.snd) base l).size = base.size

Writing a term list into an array does not change its size.

theorem Hex.SparsePoly.getD_foldl_set {R : Type u} [Zero R] {l : List (Nat × R)} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (base : Array R) (hbound : ∀ (t : Nat × R), t ∈ l → t.fst < base.size) (i : Nat) : (List.foldl (fun (acc : Array R) (t : Nat × R) => acc.setIfInBounds t.fst t.snd) base l).getD i 0 = if ∃ (t : Nat × R), t ∈ l ∧ t.fst = i then coeffList l i else base.getD i 0

Writing a sorted, in-bounds term list into an array puts each coefficient at its exponent and touches nothing else.

def Hex.SparsePoly.coeffsOfTerms {R : Type u} [Zero R] (ts : Array (Nat × R)) : Array R

Write each term of an arbitrary term array into a coefficient array sized by the largest exponent. A conversion, not a canonicaliser: with duplicate exponents the last write wins, which is what makes the round-trip hypotheses below necessary.

Equations

• Hex.SparsePoly.coeffsOfTerms ts = Array.foldl (fun (acc : Array R) (t : Nat × R) => acc.setIfInBounds t.fst t.snd) (Array.replicate (Hex.SparsePoly.termsBound ts) 0) ts

def Hex.SparsePoly.termsOfCoeffsList {R : Type u} [Zero R] [DecidableEq R] : Nat → List R → List (Nat × R)

Keep the nonzero coefficients of a coefficient list with their indices, starting at index i. Kernel-facing walk shared by termsOfCoeffs and ofDense.

Equations

• Hex.SparsePoly.termsOfCoeffsList x✝ [] = []
• Hex.SparsePoly.termsOfCoeffsList x✝ (c :: cs) = if c = 0 then Hex.SparsePoly.termsOfCoeffsList (x✝ + 1) cs else (x✝, c) :: Hex.SparsePoly.termsOfCoeffsList (x✝ + 1) cs

def Hex.SparsePoly.termsOfCoeffs {R : Type u} [Zero R] [DecidableEq R] (cs : Array R) : Array (Nat × R)

Keep the nonzero coefficients of a coefficient array with their indices.

Equations

• Hex.SparsePoly.termsOfCoeffs cs = (Hex.SparsePoly.termsOfCoeffsList 0 cs.toList).toArray

theorem Hex.SparsePoly.exp_mem_termsOfCoeffsList {R : Type u} [Zero R] [DecidableEq R] {l : List R} {i : Nat} {t : Nat × R} (ht : t ∈ termsOfCoeffsList i l) : i ≤ t.fst ∧ t.fst < i + l.length

Every index stored by the walk is at least the starting index and within the list.

theorem Hex.SparsePoly.termsOfCoeffsList_canonical {R : Type u} [Zero R] [DecidableEq R] (l : List R) (i : Nat) : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) (termsOfCoeffsList i l) ∧ ∀ (t : Nat × R), t ∈ termsOfCoeffsList i l → t.snd ≠ 0

The walk emits a canonical term list.

theorem Hex.SparsePoly.coeffList_termsOfCoeffsList {R : Type u} [Zero R] [DecidableEq R] (l : List R) (i e : Nat) : coeffList (termsOfCoeffsList i l) (i + e) = l.getD e 0

The walk stores exactly the nonzero coefficients: its coefficient at i + e is the list's value at e.

theorem Hex.SparsePoly.coeffList_termsOfCoeffsList_of_lt {R : Type u} [Zero R] [DecidableEq R] (l : List R) {i f : Nat} (hf : f < i) : coeffList (termsOfCoeffsList i l) f = 0

The walk stores nothing below its starting index.

def Hex.SparsePoly.toDense {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : 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.

Equations

• s.toDense = Hex.DensePoly.ofCoeffs (Hex.SparsePoly.coeffsOfTerms s.terms)

@[simp]

theorem Hex.SparsePoly.coeff_toDense {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (e : Nat) : s.toDense.coeff e = s.coeff e

The conversion preserves every coefficient.

noncomputable def Hex.SparsePoly.ofDense {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : 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.

Equations

• Hex.SparsePoly.ofDense p = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.termsOfCoeffsList 0 p.coeffs.toList) ⋯ ⋯

def Hex.SparsePoly.termsOfCoeffsArray {R : Type u} [Zero R] [DecidableEq R] (cs : Array R) : Array (Nat × R)

Array worker for ofDenseImpl: one indexed pass pushing the nonzero coefficients.

Equations

• Hex.SparsePoly.termsOfCoeffsArray cs = (Array.foldl (fun (st : Array (Nat × R) × Nat) (c : R) => (if c = 0 then st.fst else st.fst.push (st.snd, c), st.snd + 1)) (#[], 0) cs).fst

theorem Hex.SparsePoly.termsOfCoeffsArray_eq {R : Type u} [Zero R] [DecidableEq R] (cs : Array R) : termsOfCoeffsArray cs = (termsOfCoeffsList 0 cs.toList).toArray

The array pass agrees with the kernel-facing list walk.

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

Runtime implementation of ofDense: one array pass (value-equal to ofDense by ofDense_eq_impl, registered @[csimp]).

Equations

• Hex.SparsePoly.ofDenseImpl p = { terms := Hex.SparsePoly.termsOfCoeffsArray p.coeffs, canonical := ⋯ }

theorem Hex.SparsePoly.ofDense_eq_ofDenseImpl {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : ofDense p = ofDenseImpl p

The list walk and the array pass build the same polynomial.

@[csimp]

theorem Hex.SparsePoly.ofDense_eq_impl : @ofDense = @ofDenseImpl

Register the array pass as the compiled implementation of ofDense.

@[simp]

theorem Hex.SparsePoly.coeff_ofDense {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (e : Nat) : (ofDense p).coeff e = p.coeff e

The conversion preserves every coefficient.

theorem Hex.SparsePoly.toList_getD {R : Type u} (a : Array R) (i : Nat) (d : R) : a.toList.getD i d = a.getD i d

getD on an array agrees with getD on its list.

theorem Hex.SparsePoly.getD_coeffsOfTerms {R : Type u} [Zero R] {ts : Array (Nat × R)} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) ts.toList) (e : Nat) : (coeffsOfTerms ts).getD e 0 = coeffList ts.toList e

The dense image of a sorted term array stores exactly its coefficients.

theorem Hex.SparsePoly.coeffList_termsOfCoeffs {R : Type u} [Zero R] [DecidableEq R] (cs : Array R) (e : Nat) : coeffList (termsOfCoeffs cs).toList e = cs.getD e 0

The sparse image of a coefficient array stores exactly its coefficients.

theorem Hex.SparsePoly.terms_coeffs {R : Type u} [Zero R] [DecidableEq R] {ts : Array (Nat × R)} (h : SparsePolyCanonical ts) : termsOfCoeffs (coeffsOfTerms ts) = ts

Round trip through the dense coefficients: exact on canonical term arrays, and false without either half of the invariant (a stored zero vanishes, a duplicate is overwritten, unsorted input comes back sorted).

theorem Hex.SparsePoly.coeffs_terms {R : Type u} [Zero R] [DecidableEq R] {cs : Array R} (h : DensePolyNormalized cs) : coeffsOfTerms (termsOfCoeffs cs) = cs

Round trip through the term list: exact on trailing-zero-free coefficient arrays, and false without DensePolyNormalized (a trailing zero is not reconstructed). It is DensePoly's own invariant that makes the sparse round trip exact.

@[simp]

theorem Hex.SparsePoly.ofDense_toDense {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : ofDense s.toDense = s

Round trip on the bundled types, dense side out: unconditional, because the type carries its canonical form.

@[simp]

theorem Hex.SparsePoly.toDense_ofDense {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : (ofDense p).toDense = p

Round trip on the bundled types, sparse side out: unconditional, because DensePoly carries its trailing-zero-free form.

theorem Hex.SparsePoly.toDense_inj {R : Type u} [Zero R] [DecidableEq R] {s t : SparsePoly R} (h : s.toDense = t.toDense) : s = t

The dense conversion is injective, which is how sparse identities are transported back from dense ones.

@[simp]

theorem Hex.SparsePoly.toDense_zero {R : Type u} [Zero R] [DecidableEq R] : toDense 0 = 0

The conversion sends zero to zero.

@[simp]

theorem Hex.SparsePoly.toDense_one {R : Type u} [Zero R] [DecidableEq R] [One R] : toDense 1 = 1

The conversion sends one to one.

@[simp]

theorem Hex.SparsePoly.toDense_monomial {R : Type u} [Zero R] [DecidableEq R] (e : Nat) (c : R) : (monomial e c).toDense = DensePoly.monomial e c

The conversion sends monomials to dense monomials.

theorem Hex.SparsePoly.toDense_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t : SparsePoly S) : (s + t).toDense = s.toDense + t.toDense

The conversion is additive.

theorem Hex.SparsePoly.toDense_neg {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (s : SparsePoly S) : (-s).toDense = -s.toDense

The conversion commutes with negation.

theorem Hex.SparsePoly.ofDense_zero {R : Type u} [Zero R] [DecidableEq R] : ofDense 0 = 0

The reverse conversion sends zero to zero.

theorem Hex.SparsePoly.ofDense_one {R : Type u} [Zero R] [DecidableEq R] [One R] : ofDense 1 = 1

The reverse conversion sends one to one.

theorem Hex.SparsePoly.ofDense_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (p q : DensePoly S) : ofDense (p + q) = ofDense p + ofDense q

The reverse conversion is additive.

theorem Hex.SparsePoly.ofDense_neg {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (p : DensePoly S) : ofDense (-p) = -ofDense p

The reverse conversion commutes with negation.

theorem Hex.SparsePoly.foldl_congr' {α : Type u_1} {β : Type u_2} {l : List α} {f g : β → α → β} {i j : β} (hij : i = j) (hfg : ∀ (b : β) (a : α), a ∈ l → f b a = g b a) : List.foldl f i l = List.foldl g j l

Fold congruence pointwise on the folded function and initial value.

theorem Hex.SparsePoly.addCoeff_zero_left {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c : S) : addCoeff 0 c = c

A fresh insertion is the inserted coefficient, with no algebra assumed.

theorem Hex.SparsePoly.coeff_foldl_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] {α : Type u_1} (l : List α) (g : α → SparsePoly S) (init : SparsePoly S) (f : Nat) : (List.foldl (fun (acc : SparsePoly S) (a : α) => acc + g a) init l).coeff f = List.foldl (fun (acc : S) (a : α) => acc + (g a).coeff f) (init.coeff f) l

Coefficients of a fold of sums, sparse side.

theorem Hex.SparsePoly.coeff_mul_foldl {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t : SparsePoly S) (f : Nat) : (s * t).coeff f = List.foldl (fun (acc : S) (a : Nat × S) => acc + (mulMonomial a.fst a.snd t).coeff f) 0 s.terms.toList

The pairwise-product coefficient, reorganised as a fold of mulMonomial coefficients over the left operand's terms.

theorem Hex.SparsePoly.mul_eq_foldl {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t : SparsePoly S) : s * t = List.foldl (fun (acc : SparsePoly S) (a : Nat × S) => acc + mulMonomial a.fst a.snd t) 0 s.terms.toList

The pairwise product is the fold of monomial multiples: the shape the dense transport consumes.

theorem Hex.SparsePoly.toDense_foldl_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] {α : Type u_1} (l : List α) (g : α → SparsePoly S) (init : SparsePoly S) : (List.foldl (fun (acc : SparsePoly S) (a : α) => acc + g a) init l).toDense = List.foldl (fun (acc : DensePoly S) (a : α) => acc + (g a).toDense) init.toDense l

The dense image of a fold of sums.

theorem Hex.SparsePoly.toDense_foldl_monomial {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) : s.toDense = List.foldl (fun (acc : DensePoly S) (a : Nat × S) => acc + DensePoly.monomial a.fst a.snd) 0 s.terms.toList

A fold of dense monomials at the stored terms rebuilds the dense image.

theorem Hex.SparsePoly.toDense_mulMonomial {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (e : Nat) (c : S) (t : SparsePoly S) : (mulMonomial e c t).toDense = DensePoly.monomial e c * t.toDense

The dense image of a monomial multiple is the dense monomial product.

theorem Hex.SparsePoly.toDense_mul {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s t : 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.

theorem Hex.SparsePoly.ofDense_mul {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) : ofDense (p * q) = ofDense p * ofDense q

The multiplicative homomorphism, dense side in.

theorem Hex.SparsePoly.coeff_mul {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s t : SparsePoly S) (n : Nat) : (s * t).coeff n = s.toDense.mulCoeffSum t.toDense n

The convolution, by transport: multiplication agrees with the dense coefficient sum.

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

Multiplication is associative.

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

Multiplication is commutative.

@[simp]

theorem Hex.SparsePoly.mul_one {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s : SparsePoly S) : s * 1 = s

One is a right identity for multiplication.

@[simp]

theorem Hex.SparsePoly.one_mul {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s : SparsePoly S) : 1 * s = s

One is a left identity for multiplication.

@[simp]

theorem Hex.SparsePoly.mul_zero {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s : SparsePoly S) : s * 0 = 0

Zero absorbs on the right of multiplication.

@[simp]

theorem Hex.SparsePoly.zero_mul {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s : SparsePoly S) : 0 * s = 0

Zero absorbs on the left of multiplication.

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

Multiplication distributes over addition on the left.

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

Multiplication distributes over addition on the right.

@[simp]

theorem Hex.SparsePoly.pow_zero {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s : SparsePoly S) : s ^ 0 = 1

The zeroth power is one.

theorem Hex.SparsePoly.toDense_scale {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (c : S) (s : SparsePoly S) : (scale c s).toDense = DensePoly.scale c s.toDense

The conversion respects scalar multiplication.

@[simp]

theorem Hex.SparsePoly.toDense_C {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (c : S) : (C c).toDense = DensePoly.C c

The conversion sends constants to constants.

theorem Hex.SparsePoly.scale_eq_C_mul {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (c : S) (s : SparsePoly S) : scale c s = C c * s

Scalar multiplication is multiplication by the constant.

theorem Hex.SparsePoly.monomial_mul_monomial {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (a b : Nat) (c d : S) : monomial a c * monomial b d = monomial (a + b) (c * d)

Sparse monomials multiply exponentwise, by transport.

theorem Hex.SparsePoly.pow_succ {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (s : SparsePoly S) (n : Nat) : s ^ (n + 1) = s * s ^ n

The power recurrence: with pow_zero this characterises the binary powering completely, and together with coeff_mul it is what the SPEC's coeff_pow obligation reduces to.

theorem Hex.SparsePoly.exp_le_back {R : Type u} [Zero R] [DecidableEq R] {s : SparsePoly R} {t : Nat × R} (hback : s.terms.back? = some t) (u : Nat × R) : u ∈ s.terms.toList → u.fst ≤ t.fst

On a sorted term list the last stored exponent dominates.

theorem Hex.SparsePoly.leadingCoeff_eq_coeff {R : Type u} [Zero R] [DecidableEq R] {s : SparsePoly R} {t : Nat × R} (hback : s.terms.back? = some t) : s.leadingCoeff = s.coeff t.fst

The leading coefficient is the coefficient at the last stored exponent.

theorem Hex.SparsePoly.size_toDense_eq {R : Type u} [Zero R] [DecidableEq R] {s : SparsePoly R} {t : Nat × R} (hback : s.terms.back? = some t) : s.toDense.size = t.fst + 1

The dense image stores exactly degree + 1 coefficients.

@[simp]

theorem Hex.SparsePoly.degree?_toDense {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : s.toDense.degree? = s.degree?

The degree boundary transports: a leading coefficient is a coefficient at the degree, and coeff_toDense alone says nothing about where the degree is.

@[simp]

theorem Hex.SparsePoly.leadingCoeff_toDense {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : s.toDense.leadingCoeff = s.leadingCoeff

The leading coefficient transports through the dense conversion.

def Hex.SparsePoly.Monic {R : Type u} [Zero R] [DecidableEq R] [One R] (s : SparsePoly R) : Prop

A sparse polynomial is monic when its leading coefficient is 1, matching the DensePoly convention.

Equations

• s.Monic = (s.leadingCoeff = 1)

@[instance_reducible]

instance Hex.SparsePoly.instDecidableMonic {R : Type u} [Zero R] [DecidableEq R] [One R] (s : SparsePoly R) : Decidable s.Monic

Equations

• s.instDecidableMonic = Hex.SparsePoly.instDecidableMonic._aux_1 s

@[simp]

theorem Hex.SparsePoly.monic_toDense {R : Type u} [Zero R] [DecidableEq R] [One R] (s : SparsePoly R) : s.toDense.Monic ↔ s.Monic

Monicity transports through the dense conversion.