Computable multivariate polynomials

Polynomials of the form α₁ * m₁ + α₂ * m₂ + ... + αₖ * mₖ where αᵢ is any semiring and mᵢ is a CMvMonomial.

This is implemented as a wrapper around CPoly.Lawful, which ensures that all stored coefficients are non-zero.

This file contains the core type definition and basic operations. Higher-level definitions that depend on ring instances (monomial orders, rename, aeval, etc.) are in CMvPolynomial.lean. The CommSemiring and CommRing instances are in MvPolyEquiv.lean.

Main definitions

• CPoly.CMvPolynomial n R: The type of multivariate polynomials in n variables with coefficients in R.
• CPoly.CMvPolynomial.C: Constant polynomial constructor.
• CPoly.CMvPolynomial.X: Variable polynomial constructor.
• CPoly.CMvPolynomial.monomial: Monomial constructor.
• CPoly.CMvPolynomial.coeff: Extract the coefficient of a monomial.
• CPoly.CMvPolynomial.eval₂, CPoly.CMvPolynomial.eval: Polynomial evaluation.
• CPoly.CMvPolynomial.eval₂Horner, CPoly.CMvPolynomial.evalHorner: Polynomial evaluation using Horner's method.
• CPoly.CMvPolynomial.support, CPoly.CMvPolynomial.totalDegree, CPoly.CMvPolynomial.degreeOf, CPoly.CMvPolynomial.degrees, CPoly.CMvPolynomial.vars: Degree and support queries.

@[reducible, inline]

abbrev CPoly.CMvPolynomial (n : ℕ) (R : Type u_1) [Zero R] : Type u_1

A computable multivariate polynomial in n variables with coefficients in R.

def CPoly.CMvPolynomial.C {n : ℕ} {R : Type u_2} [BEq R] [LawfulBEq R] [Zero R] (c : R) : CMvPolynomial n R

Construct a constant polynomial.

def CPoly.CMvPolynomial.X {n : ℕ} {R : Type u_2} [Zero R] [One R] [BEq R] [LawfulBEq R] (i : Fin n) : CMvPolynomial n R

Construct the polynomial $X_i$.

def CPoly.CMvPolynomial.coeff {R : Type u_2} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : CMvPolynomial n R) : R

Extract the coefficient of a monomial.

theorem CPoly.CMvPolynomial.ext {R : Type u_1} {n : ℕ} [Zero R] (p q : CMvPolynomial n R) (h : ∀ (m : CMvMonomial n), coeff m p = coeff m q) : p = q

Extensionality: two polynomials are equal if all their coefficients are equal.

theorem CPoly.CMvPolynomial.ext_iff {R : Type u_1} {n : ℕ} [Zero R] {p q : CMvPolynomial n R} : p = q ↔ ∀ (m : CMvMonomial n), coeff m p = coeff m q

@[simp]

theorem CPoly.CMvPolynomial.fromUnlawful_zero {R : Type u_1} [BEq R] [LawfulBEq R] {n : ℕ} [Zero R] : Lawful.fromUnlawful 0 = 0

@[simp]

theorem CPoly.CMvPolynomial.add_getD? {R : Type u_1} [BEq R] [LawfulBEq R] {n : ℕ} [CommSemiring R] {m : CMvMonomial n} {p q : CMvPolynomial n R} : (↑(p + q))[m]?.getD 0 = (↑p)[m]?.getD 0 + (↑q)[m]?.getD 0

@[simp]

theorem CPoly.CMvPolynomial.coeff_add {R : Type u_1} [BEq R] [LawfulBEq R] {n : ℕ} [CommSemiring R] {m : CMvMonomial n} {p q : CMvPolynomial n R} : coeff m (p + q) = coeff m p + coeff m q

theorem CPoly.CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful₀ {R : Type u_1} [BEq R] [LawfulBEq R] {n : ℕ} [CommSemiring R] {t : List (CMvMonomial n × R)} {f : CMvMonomial n → R → Unlawful n R} (init : Unlawful n R) : Lawful.fromUnlawful (List.foldl (fun (u : Unlawful n R) (term : CMvMonomial n × R) => f term.1 term.2 + u) init t) = List.foldl (fun (l : Lawful n R) (term : CMvMonomial n × R) => Lawful.fromUnlawful (f term.1 term.2) + l) (Lawful.fromUnlawful init) t

Auxiliary lemma showing that conversion from unlawful polynomials respects the sum fold.

theorem CPoly.CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful {R : Type u_1} [BEq R] [LawfulBEq R] {n : ℕ} [CommSemiring R] {t : Unlawful n R} {f : CMvMonomial n → R → Unlawful n R} : Lawful.fromUnlawful (Std.ExtTreeMap.foldl (fun (u : Unlawful n R) (m : CMvMonomial n) (c : R) => f m c + u) 0 t) = Std.ExtTreeMap.foldl (fun (l : Lawful n R) (m : CMvMonomial n) (c : R) => Lawful.fromUnlawful (f m c) + l) 0 t

Auxiliary lemma showing that conversion from unlawful polynomials respects the fold over terms.

def CPoly.CMvPolynomial.eval₂ {R : Type u_2} {S : Type u_3} {n : ℕ} [Semiring R] [CommSemiring S] : (R →+* S) → (Fin n → S) → CMvPolynomial n R → S

Evaluate a polynomial at a point given by a ring homomorphism f and variable assignments vs.

@[reducible, inline]

abbrev CPoly.CMvPolynomial.HornerTerm (n : ℕ) (S : Type u_2) : Type u_2

Term representation used by the fixed-order multivariate Horner evaluator.

@[reducible, inline]

abbrev CPoly.CMvPolynomial.HornerGroup (n : ℕ) (S : Type u_2) : Type u_2

Terms grouped by one variable exponent.

def CPoly.CMvPolynomial.hornerExponent {n : ℕ} (k : ℕ) (m : CMvMonomial n) : ℕ

Read the exponent for a variable index represented as a natural number.

def CPoly.CMvPolynomial.insertHornerTerm {n : ℕ} {S : Type u_2} (exponent : ℕ) (term : HornerTerm n S) : List (HornerGroup n S) → List (HornerGroup n S)

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

def CPoly.CMvPolynomial.insertHornerGroupDesc {n : ℕ} {S : Type u_2} (group : HornerGroup n S) : List (HornerGroup n S) → List (HornerGroup n S)

Insert an exponent group into descending exponent order.

def CPoly.CMvPolynomial.collectHornerGroups {n : ℕ} {S : Type u_2} (k : ℕ) (terms : List (HornerTerm n S)) : List (HornerGroup n S)

Collect terms into association-list groups keyed by the current variable exponent.

def CPoly.CMvPolynomial.sortHornerGroups {n : ℕ} {S : Type u_2} (groups : List (HornerGroup n S)) : List (HornerGroup n S)

Sort exponent groups from high exponent to low exponent.

def CPoly.CMvPolynomial.hornerGroups {n : ℕ} {S : Type u_2} (k : ℕ) (terms : List (HornerTerm n S)) : List (HornerGroup n S)

Group terms by the current variable exponent, sorted from high to low exponent.

def CPoly.CMvPolynomial.evalSparseHornerGroups {S : Type u_2} [CommSemiring S] (x : S) : List (ℕ × S) → S

Sparse Horner fold for already-evaluated coefficient groups.

def CPoly.CMvPolynomial.eval₂HornerTerms {n : ℕ} {S : Type u_2} [CommSemiring S] (xs : ℕ → S) : ℕ → ℕ → List (HornerTerm n S) → S

Evaluate sparse multivariate terms by fixed-order Horner in variables 0, 1, ..., n-1.

def CPoly.CMvPolynomial.eval₂Horner {R : Type u_2} {S : Type u_3} {n : ℕ} [Semiring R] [CommSemiring S] : (R →+* S) → (Fin n → S) → CMvPolynomial n R → S

Evaluate a polynomial using fixed-order multivariate Horner evaluation.

def CPoly.CMvPolynomial.eval {R : Type u_2} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvPolynomial n R → R

Evaluate a polynomial at a given point.

def CPoly.CMvPolynomial.evalHorner {R : Type u_2} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvPolynomial n R → R

Evaluate a polynomial at a given point using fixed-order multivariate Horner evaluation.

def CPoly.CMvPolynomial.support {R : Type u_2} {n : ℕ} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n →₀ ℕ)

The support of a polynomial (set of monomials with non-zero coefficients), represented as Finsupps.

def CPoly.CMvPolynomial.totalDegree {R : Type u_2} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ

The total degree of a polynomial (maximum total degree of its monomials).

def CPoly.CMvPolynomial.degreeOf {R : Type u_2} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ

The degree of a polynomial in a specific variable.

def CPoly.CMvPolynomial.monomial {n : ℕ} {R : Type u_2} [BEq R] [LawfulBEq R] [Zero R] (m : CMvMonomial n) (c : R) : CMvPolynomial n R

Construct a monomial c * m as a CMvPolynomial n R.

Creates a polynomial with a single monomial term. If c = 0, returns the zero polynomial.

def CPoly.CMvPolynomial.degrees {n : ℕ} {R : Type u_2} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n)

Multiset of all variable degrees appearing in the polynomial.

Each variable i appears degreeOf i p times in the multiset.

theorem CPoly.CMvPolynomial.degreeOf_eq_count_degrees {n : ℕ} {R : Type u_2} [Zero R] (i : Fin n) (p : CMvPolynomial n R) : degreeOf i p = Multiset.count i p.degrees

degreeOf is the multiplicity of a variable in degrees.

def CPoly.CMvPolynomial.vars {n : ℕ} {R : Type u_2} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n)

Extract the set of variables that appear in a polynomial.

Returns the set of variable indices i : Fin n such that degreeOf i p > 0.

def CPoly.CMvPolynomial.restrictBy {n : ℕ} {R : Type u_2} [BEq R] [LawfulBEq R] [Zero R] (keep : CMvMonomial n → Prop) [DecidablePred keep] (p : CMvPolynomial n R) : CMvPolynomial n R

Filter a polynomial, keeping only monomials for which keep m is true.

def CPoly.CMvPolynomial.restrictTotalDegree {n : ℕ} {R : Type u_2} [BEq R] [LawfulBEq R] [Zero R] (d : ℕ) (p : CMvPolynomial n R) : CMvPolynomial n R

Restrict polynomial to monomials with total degree ≤ d.

Filters out all monomials where m.totalDegree > d.

def CPoly.CMvPolynomial.restrictDegree {n : ℕ} {R : Type u_2} [BEq R] [LawfulBEq R] [Zero R] (d : ℕ) (p : CMvPolynomial n R) : CMvPolynomial n R

Restrict polynomial to monomials whose degree in each variable is ≤ d.

Filters out all monomials where m.degreeOf i > d for some variable i.