def Hex.MvPoly.removeVar {n : Nat} (i : Fin (n + 1)) (m : Mono (n + 1)) : Mono n

Remove coordinate i from an exponent vector. This is the explicit Mathlib-free form of precomposition by Fin.succAbove i.

Equations

• Hex.MvPoly.removeVar i m = Hex.Vector.ofFn' fun (j : Fin n) => if ↑j < ↑i then m[⟨↑j, ⋯⟩] else m[⟨↑j + 1, ⋯⟩]

def Hex.MvPoly.insertVar {n : Nat} (i : Fin (n + 1)) (e : Nat) (m : Mono n) : Mono (n + 1)

Insert exponent e at coordinate i.

Equations

• Hex.MvPoly.insertVar i e m = Hex.Vector.ofFn' fun (j : Fin (n + 1)) => if hsame : ↑j = ↑i then e else if hlt : ↑j < ↑i then m[⟨↑j, ⋯⟩] else m[⟨↑j - 1, ⋯⟩]

@[simp]

theorem Hex.MvPoly.degreeOf_insertVar {n : Nat} (i : Fin (n + 1)) (e : Nat) (m : Mono n) : Mono.degreeOf i (insertVar i e m) = e

The inserted variable has the supplied exponent.

@[simp]

theorem Hex.MvPoly.removeVar_insertVar {n : Nat} (i : Fin (n + 1)) (e : Nat) (m : Mono n) : removeVar i (insertVar i e m) = m

Removing a freshly inserted variable recovers the original monomial.

@[simp]

theorem Hex.MvPoly.insertVar_removeVar {n : Nat} (i : Fin (n + 1)) (m : Mono (n + 1)) : insertVar i (Mono.degreeOf i m) (removeVar i m) = m

Re-inserting a removed variable with its old exponent recovers the original monomial.

theorem Hex.MvPoly.insertVar_inj {n : Nat} (i : Fin (n + 1)) (e d : Nat) (m k : Mono n) : insertVar i e m = insertVar i d k ↔ e = d ∧ m = k

Inserting a variable is jointly injective in the new exponent and the remaining monomial.

def Hex.MvPoly.toUnivariateSize {n : Nat} {R : Type u} (i : Fin (n + 1)) (terms : List (Mono (n + 1) × R)) : Nat

Array length needed to accumulate every exponent bucket.

Equations

• Hex.MvPoly.toUnivariateSize i terms = List.foldl (fun (bound : Nat) (term : Hex.Mono (n + 1) × R) => max bound (Hex.Mono.degreeOf i term.fst + 1)) 0 terms

def Hex.MvPoly.toUnivariateStep {n : Nat} {R : Type u} {cmp' : Mono n → Mono n → Ordering} [Lean.Grind.Semiring R] [DecidableEq R] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (i : Fin (n + 1)) (coeffs : Array (MvPoly n R cmp')) (term : Mono (n + 1) × R) : Array (MvPoly n R cmp')

Accumulate one source term into its dense univariate coefficient bucket. The caller must ensure that the term's selected degree is below coeffs.size; otherwise Array.set! leaves the array unchanged.

Equations

• Hex.MvPoly.toUnivariateStep i coeffs term = coeffs.set! (Hex.Mono.degreeOf i term.fst) ((coeffs.getD (Hex.Mono.degreeOf i term.fst) 0).addMonomial (Hex.MvPoly.removeVar i term.fst) term.snd)

def Hex.MvPoly.toUnivariateCoeffs {n : Nat} {R : Type u} {cmp' : Mono n → Mono n → Ordering} [Lean.Grind.Semiring R] [DecidableEq R] [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (i : Fin (n + 1)) (terms : List (Mono (n + 1) × R)) : Array (MvPoly n R cmp')

Dense coefficient array obtained by two linear passes over sparse terms: one to determine the array size and one to populate its buckets.

Equations

• One or more equations did not get rendered due to their size.

def Hex.MvPoly.toUnivariate {n : Nat} {R : Type u} {cmp : Mono (n + 1) → Mono (n + 1) → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin (n + 1)) (cmp' : Mono n → Mono n → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (p : MvPoly (n + 1) R cmp) : DensePoly (MvPoly n R cmp')

Coefficients of p as a dense univariate polynomial in variable i. Each coefficient is a polynomial in the remaining n variables.

Equations

• Hex.MvPoly.toUnivariate i cmp' p = Hex.DensePoly.ofCoeffs (Hex.MvPoly.toUnivariateCoeffs i p.termsList)

def Hex.MvPoly.ofUnivariate {n : Nat} {R : Type u} {cmp : Mono (n + 1) → Mono (n + 1) → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin (n + 1)) (cmp' : Mono n → Mono n → Ordering) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (q : DensePoly (MvPoly n R cmp')) : MvPoly (n + 1) R cmp

Inverse of toUnivariate, reinserting variable i.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.MvPoly.toUnivariate_coeff {n : Nat} {R : Type u} {cmp : Mono (n + 1) → Mono (n + 1) → Ordering} {cmp' : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin (n + 1)) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (p : MvPoly (n + 1) R cmp) (e : Nat) (m : Mono n) : coeff m ((toUnivariate i cmp' p).coeff e) = coeff (insertVar i e m) p

A recursive-view coefficient is the source coefficient indexed by the inserted main-variable exponent.

theorem Hex.MvPoly.ofUnivariate_coeff {n : Nat} {R : Type u} {cmp : Mono (n + 1) → Mono (n + 1) → Ordering} {cmp' : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin (n + 1)) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (q : DensePoly (MvPoly n R cmp')) (e : Nat) (m : Mono n) : coeff (insertVar i e m) (ofUnivariate i cmp' q) = coeff m (q.coeff e)

Reassembly sends a recursive coefficient back to its inserted multivariate monomial.

theorem Hex.MvPoly.ofUnivariate_toUnivariate {n : Nat} {R : Type u} {cmp : Mono (n + 1) → Mono (n + 1) → Ordering} {cmp' : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin (n + 1)) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (p : MvPoly (n + 1) R cmp) : ofUnivariate i cmp' (toUnivariate i cmp' p) = p

Converting to the recursive view and back is the identity.

theorem Hex.MvPoly.toUnivariate_ofUnivariate {n : Nat} {R : Type u} {cmp : Mono (n + 1) → Mono (n + 1) → Ordering} {cmp' : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (i : Fin (n + 1)) [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] (q : DensePoly (MvPoly n R cmp')) : toUnivariate i cmp' (ofUnivariate i cmp' q) = q

Converting a recursive polynomial to multivariate form and back is the identity.