def Hex.MvPoly.eval₂ {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) (p : MvPoly n R cmp) : S

Evaluate coefficients through f and variables through x. Powers are computed by repeated squaring in Mono.prod.

Equations

• Hex.MvPoly.eval₂ f x p = Hex.MvPoly.foldTerms (fun (acc : S) (m : Hex.Mono n) (c : R) => acc + f c * Hex.Mono.prod x m) 0 p

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

Evaluate a polynomial at x.

Equations

• Hex.MvPoly.eval x p = Hex.MvPoly.eval₂ id x p

@[reducible, inline]

abbrev Hex.MvPoly.HornerTerm (n : Nat) (S : Type v) : Type v

A term whose coefficient has already been mapped into the target semiring.

Equations

• Hex.MvPoly.HornerTerm n S = (Hex.Mono n × S)

@[reducible, inline]

abbrev Hex.MvPoly.HornerGroup (n : Nat) (S : Type v) : Type v

Terms sharing one exponent in the variable currently being evaluated.

Equations

• Hex.MvPoly.HornerGroup n S = (Nat × List (Hex.MvPoly.HornerTerm n S))

def Hex.MvPoly.hornerExponent {n : Nat} (k : Nat) (m : Mono n) : Nat

Read an exponent using a natural variable index, returning zero when the index is out of range.

Equations

• Hex.MvPoly.hornerExponent k m = if h : k < n then m[⟨k, h⟩] else 0

def Hex.MvPoly.insertHornerTerm {n : Nat} {S : Type v} (exponent : Nat) (term : HornerTerm n S) : List (HornerGroup n S) → List (HornerGroup n S)

Add a term to an association list keyed by one variable exponent.

Equations

• Hex.MvPoly.insertHornerTerm exponent term [] = [(exponent, [term])]
• Hex.MvPoly.insertHornerTerm exponent term (group :: groups) = if group.fst = exponent then (group.fst, term :: group.snd) :: groups else group :: Hex.MvPoly.insertHornerTerm exponent term groups

def Hex.MvPoly.insertHornerGroupDesc {n : Nat} {S : Type v} (group : HornerGroup n S) : List (HornerGroup n S) → List (HornerGroup n S)

Insert an exponent group into descending exponent order.

Equations

• Hex.MvPoly.insertHornerGroupDesc group [] = [group]
• Hex.MvPoly.insertHornerGroupDesc group (group_1 :: groups) = if group_1.fst < group.fst then group :: group_1 :: groups else group_1 :: Hex.MvPoly.insertHornerGroupDesc group groups

def Hex.MvPoly.collectHornerGroups {n : Nat} {S : Type v} (k : Nat) (terms : List (HornerTerm n S)) : List (HornerGroup n S)

Collect terms into groups keyed by their exponent at variable k.

Equations

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

def Hex.MvPoly.sortHornerGroups {n : Nat} {S : Type v} (groups : List (HornerGroup n S)) : List (HornerGroup n S)

Sort exponent groups from high exponent to low exponent.

Equations

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

def Hex.MvPoly.hornerGroups {n : Nat} {S : Type v} (k : Nat) (terms : List (HornerTerm n S)) : List (HornerGroup n S)

Group terms by one variable exponent, ordered from high to low.

Equations

• Hex.MvPoly.hornerGroups k terms = Hex.MvPoly.sortHornerGroups (Hex.MvPoly.collectHornerGroups k terms)

def Hex.MvPoly.hornerStep {S : Type v} [Lean.Grind.Semiring S] (x : S) (state group : Nat × S) : Nat × S

Advance one descending sparse-Horner exponent group.

Equations

• Hex.MvPoly.hornerStep x state group = (group.fst, state.snd * Hex.Mono.powBySq x (state.fst - group.fst) + group.snd)

def Hex.MvPoly.evalSparseHornerGroups {S : Type v} [Lean.Grind.Semiring S] (x : S) : List (Nat × S) → S

Sparse Horner fold over already-evaluated coefficient groups. Callers must supply groups in descending exponent order. Missing exponents are skipped with repeated-squaring powers.

Equations

• Hex.MvPoly.evalSparseHornerGroups x [] = 0
• Hex.MvPoly.evalSparseHornerGroups x (group :: groups) = (List.foldl (Hex.MvPoly.hornerStep x) group groups).snd * Hex.Mono.powBySq x (List.foldl (Hex.MvPoly.hornerStep x) group groups).fst

def Hex.MvPoly.eval₂HornerTerms {n : Nat} {S : Type v} [Lean.Grind.Semiring S] (xs : Nat → S) : Nat → Nat → List (HornerTerm n S) → S

Evaluate sparse terms by fixed-order Horner in variables 0, 1, ..., n - 1. fuel is the number of variables left.

Equations

• One or more equations did not get rendered due to their size.
• Hex.MvPoly.eval₂HornerTerms xs 0 x✝¹ x✝ = List.foldl (fun (acc : S) (term : Hex.MvPoly.HornerTerm n S) => acc + term.snd) 0 x✝

def Hex.MvPoly.eval₂Horner {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.CommSemiring S] (f : R → S) (x : Fin n → S) (p : MvPoly n R cmp) : S

Evaluate using fixed-variable-order sparse Horner evaluation. The target semiring is commutative because variable nesting may reorder factors.

Equations

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

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

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

Equations

• Hex.MvPoly.evalHorner x p = Hex.MvPoly.eval₂Horner id x p

def Hex.MvPoly.eraseAssigned {n : Nat} {R : Type u} (s : Fin n → Option R) (m : Mono n) : Mono n

Erase the exponents of variables assigned by s.

Equations

• Hex.MvPoly.eraseAssigned s m = Hex.Vector.ofFn' fun (i : Fin n) => if (s i).isSome = true then 0 else m[i]

def Hex.MvPoly.partialEval {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] (s : Fin n → Option R) (p : MvPoly n R cmp) : 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.

Equations

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

theorem Hex.MvPoly.eval₂_eq {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) (p : MvPoly n R cmp) : eval₂ f x p = List.foldl (fun (acc : S) (term : Mono n × R) => acc + f term.snd * Mono.prod x term.fst) 0 p.termsList

Evaluation is the ordered term fold of mapped coefficients times monomial values.

theorem Hex.MvPoly.eval_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] (x : Fin n → R) (p : MvPoly n R cmp) : eval x p = List.foldl (fun (acc : R) (term : Mono n × R) => acc + term.snd * Mono.prod x term.fst) 0 p.termsList

Same-ring evaluation is the ordered term fold with unchanged coefficients.

theorem Hex.MvPoly.eval₂Horner_eq {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.CommSemiring S] (f : R → S) (x : Fin n → S) (p : MvPoly n R cmp) : eval₂Horner f x p = eval₂ f x p

Sparse Horner evaluation agrees with direct term evaluation.

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

Same-ring sparse Horner evaluation agrees with ordinary evaluation.

theorem Hex.MvPoly.eval₂_eq_foldl_monomials {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) (p : MvPoly n R cmp) : eval₂ f x p = List.foldl (fun (acc : S) (m : Mono n) => acc + f (coeff m p) * Mono.prod x m) 0 p.monomials

Evaluation is the fold over the canonical support of mapped coefficients times monomial values.

theorem Hex.MvPoly.eval₂_eq_foldl_of_superset {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) (hf0 : f 0 = 0) (p : MvPoly n R cmp) (L : List (Mono n)) (hL : L.Nodup) (hsub : ∀ (m : Mono n), m ∈ p.monomials → m ∈ L) : eval₂ f x p = List.foldl (fun (acc : S) (m : Mono n) => acc + f (coeff m p) * Mono.prod x m) 0 L

Evaluation may be written as a fold over any duplicate-free list of monomials containing the support, provided f fixes zero.

theorem Hex.MvPoly.eval₂_zero {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) (hf0 : f 0 = 0) : eval₂ f x 0 = 0

The zero polynomial evaluates to zero.

theorem Hex.MvPoly.eval₂_addMonomial {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) [Add R] [BEq R] [LawfulBEq R] [DecidableEq R] (hf0 : f 0 = 0) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (p : MvPoly n R cmp) (m : Mono n) (c : R) : eval₂ f x (p.addMonomial m c) = eval₂ f x p + f c * Mono.prod x m

Adding a monomial adds its mapped value, for an additive f fixing zero.

theorem Hex.MvPoly.eval₂_ofTerms {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) [Add R] [BEq R] [LawfulBEq R] [DecidableEq R] (hf0 : f 0 = 0) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (ts : List (Mono n × R)) : eval₂ f x (ofTerms ts) = List.foldl (fun (acc : S) (t : Mono n × R) => acc + f t.snd * Mono.prod x t.fst) 0 ts

Building a polynomial from a term list evaluates to the fold of the mapped terms, for an additive f fixing zero.

theorem Hex.MvPoly.eval₂_add {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [DecidableEq R] [Lean.Grind.Semiring S] (f : R → S) (x : Fin n → S) (hf0 : f 0 = 0) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (p q : MvPoly n R cmp) : eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q

Evaluation is additive, for an additive f fixing zero.