3.5. Evaluation and structural operations🔗

Direct evaluation folds the sparse support, using repeated squaring for each exponent. Sparse Horner evaluation groups terms by variable exponent, and is proven equal to the direct evaluator.

def

Hex.MvPoly.eval.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] (x : Fin n → R)
  (p : Hex.MvPoly n R cmp) : R
Hex.MvPoly.eval.{u} {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.Semiring R] (x : Fin n → R)
  (p : Hex.MvPoly n R cmp) : R

Evaluate a polynomial at x.

def

Hex.MvPoly.evalHorner.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommSemiring R] (x : Fin n → R)
  (p : Hex.MvPoly n R cmp) : R
Hex.MvPoly.evalHorner.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommSemiring R]
  (x : Fin n → R)
  (p : Hex.MvPoly n R cmp) : R

Evaluate at x using fixed-variable-order sparse Horner evaluation.

theorem

Hex.MvPoly.evalHorner_eq.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.CommSemiring R] (x : Fin n → R)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly.evalHorner x p = Hex.MvPoly.eval x p
Hex.MvPoly.evalHorner_eq.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.CommSemiring R]
  (x : Fin n → R)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly.evalHorner x p =
    Hex.MvPoly.eval x p

Same-ring sparse Horner evaluation agrees with ordinary evaluation.

The structural API changes variables, substitutes polynomials, projects homogeneous pieces, differentiates, or partially evaluates selected variables while preserving canonical form.

def

Hex.MvPoly.reorder.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [Lean.Grind.Semiring R]
  [DecidableEq R] (p : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp'
Hex.MvPoly.reorder.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp']
  [Std.LawfulEqCmp cmp']
  [Lean.Grind.Semiring R] [DecidableEq R]
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp'

Rebuild a polynomial under a different monomial comparator.

def

Hex.MvPoly.rename.{u} {n k : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] (cmp' : Hex.Mono k → Hex.Mono k → Ordering)
  [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] [Lean.Grind.Semiring R]
  [DecidableEq R] (f : Fin n → Fin k) (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly k R cmp'
Hex.MvPoly.rename.{u} {n k : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (cmp' :
    Hex.Mono k → Hex.Mono k → Ordering)
  [Std.TransCmp cmp']
  [Std.LawfulEqCmp cmp']
  [Lean.Grind.Semiring R] [DecidableEq R]
  (f : Fin n → Fin k)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly k R cmp'

Rename variables, adding exponents in fibres and combining all resulting term collisions.

def

Hex.MvPoly.derivative.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] [NatCast R] [Add R] [Mul R]
  [DecidableEq R] (i : Fin n) (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp
Hex.MvPoly.derivative.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] [NatCast R] [Add R] [Mul R]
  [DecidableEq R] (i : Fin n)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Formal derivative with respect to variable i.

def

Hex.MvPoly.homogeneousComponent.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (d : ℕ)
  (p : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.homogeneousComponent.{u}
  {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.Semiring R] [DecidableEq R]
  (d : ℕ) (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Homogeneous component of total degree d.

def

Hex.MvPoly.subst.{u} {n k : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  {targetCmp : Hex.Mono k → Hex.Mono k → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp]
  [Std.LawfulEqCmp targetCmp] [Lean.Grind.Semiring R] [DecidableEq R]
  (f : Fin n → Hex.MvPoly k R targetCmp) (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly k R targetCmp
Hex.MvPoly.subst.{u} {n k : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  {targetCmp :
    Hex.Mono k → Hex.Mono k → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Std.TransCmp targetCmp]
  [Std.LawfulEqCmp targetCmp]
  [Lean.Grind.Semiring R] [DecidableEq R]
  (f : Fin n → Hex.MvPoly k R targetCmp)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly k R targetCmp

Substitute polynomials for variables without changing the coefficient type.

def

Hex.MvPoly.partialEval.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R]
  (s : Fin n → Option R) (p : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.partialEval.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.Semiring R] [DecidableEq R]
  (s : Fin n → Option R)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Evaluate the variables assigned by s, leaving all other variables in the same ambient polynomial ring. Terms that collide are combined.

For algorithms that recurse on the number of variables, Hex.MvPoly.toUnivariate views a polynomial as a dense polynomial in one selected variable whose coefficients are sparse polynomials in the remaining variables. Hex.MvPoly.ofUnivariate is its proven inverse.

def

Hex.MvPoly.toUnivariate.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R]
  [DecidableEq R] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp']
  [Std.LawfulEqCmp cmp'] (p : Hex.MvPoly (n + 1) R cmp) :
  Hex.DensePoly (Hex.MvPoly n R cmp')
Hex.MvPoly.toUnivariate.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Lean.Grind.Semiring R] [DecidableEq R]
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp']
  [Std.LawfulEqCmp cmp']
  (p : Hex.MvPoly (n + 1) R cmp) :
  Hex.DensePoly (Hex.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.

theorem

Hex.MvPoly.ofUnivariate_toUnivariate.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.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 : Hex.MvPoly (n + 1) R cmp) :
  Hex.MvPoly.ofUnivariate i cmp' (Hex.MvPoly.toUnivariate i cmp' p) = p
Hex.MvPoly.ofUnivariate_toUnivariate.{u}
  {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.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 : Hex.MvPoly (n + 1) R cmp) :
  Hex.MvPoly.ofUnivariate i cmp'
      (Hex.MvPoly.toUnivariate i cmp' p) =
    p

Converting to the recursive view and back is the identity.

3.5.1. Worked example🔗

The example builds x² + 2xy + 3, inspects its sparse support, evaluates it, and differentiates with respect to x.

open Hex Hex.MvPoly

namespace HexMvPolyChapter

abbrev P := MvPoly 2 Int Mono.lex

def x : P := X 0
def y : P := X 1
def p : P :=
  x ^ 2 + (C 2 * x) * y + C 3

#guard p.termCount = 3
#guard p.coeff #v[2, 0] = 1
#guard p.coeff #v[1, 1] = 2
#guard p.totalDegree = 2
#guard eval (fun i => if i = 0 then 2 else 5) p = 27
#guard derivative 0 p =
  C 2 * x + C 2 * y

end HexMvPolyChapter