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.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) [Zero R] : Type

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

Equations

• CPoly.CMvPolynomial n R = CPoly.Lawful n R

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

Construct a constant polynomial.

Equations

• CPoly.CMvPolynomial.C c = CPoly.Lawful.C c

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

Construct the polynomial $X_i$.

Equations

• CPoly.CMvPolynomial.X i = CPoly.Lawful.fromUnlawful (CPoly.Unlawful.ofList [(Vector.ofFn fun (j : Fin n) => if j = i then 1 else 0, 1)])

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

Extract the coefficient of a monomial.

Equations

• CPoly.CMvPolynomial.coeff m p = (↑p)[m]?.getD 0

theorem CPoly.CMvPolynomial.ext {R : Type} {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} {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} [BEq R] [LawfulBEq R] {n : ℕ} [Zero R] : Lawful.fromUnlawful 0 = 0

@[simp]

theorem CPoly.CMvPolynomial.add_getD? {R : Type} [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} [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} [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} [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 S : Type} {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.

Equations

• CPoly.CMvPolynomial.eval₂ f vs p = Std.ExtTreeMap.foldl (fun (s : S) (m : CPoly.CMvMonomial n) (c : R) => f c * CPoly.MonoR.evalMonomial vs m + s) 0 ↑p

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

Evaluate a polynomial at a given point.

Equations

• CPoly.CMvPolynomial.eval = CPoly.CMvPolynomial.eval₂ (RingHom.id R)

def CPoly.CMvPolynomial.support {R : Type} {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.

Equations

• p.support = (List.map CPoly.CMvMonomial.toFinsupp (CPoly.Lawful.monomials p)).toFinset

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

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

Equations

• p.totalDegree = (List.map CPoly.CMvMonomial.toFinsupp (CPoly.Lawful.monomials p)).toFinset.sup fun (s : Fin n →₀ ℕ) => s.sum fun (x : Fin n) (e : ℕ) => e

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

The degree of a polynomial in a specific variable.

Equations

• CPoly.CMvPolynomial.degreeOf i p = Multiset.count i ((List.map CPoly.CMvMonomial.toFinsupp (CPoly.Lawful.monomials p)).toFinset.sup fun (s : Fin n →₀ ℕ) => Finsupp.toMultiset s)

def CPoly.CMvPolynomial.monomial {n : ℕ} {R : Type} [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.

Equations

• CPoly.CMvPolynomial.monomial m c = if (c == 0) = true then 0 else CPoly.Lawful.fromUnlawful (CPoly.Unlawful.ofList [(m, c)])

def CPoly.CMvPolynomial.degrees {n : ℕ} {R : Type} [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.

Equations

• p.degrees = ∑ i : Fin n, Multiset.replicate (CPoly.CMvPolynomial.degreeOf i p) i

theorem CPoly.CMvPolynomial.degreeOf_eq_count_degrees {n : ℕ} {R : Type} [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} [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.

Equations

• p.vars = {i : Fin n | 0 < CPoly.CMvPolynomial.degreeOf i p}

def CPoly.CMvPolynomial.restrictBy {n : ℕ} {R : Type} [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.

Equations

• CPoly.CMvPolynomial.restrictBy keep p = CPoly.Lawful.fromUnlawful (Std.ExtTreeMap.filter (fun (m : CPoly.CMvMonomial n) (x : R) => decide (keep m)) ↑p)

def CPoly.CMvPolynomial.restrictTotalDegree {n : ℕ} {R : Type} [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.

Equations

• CPoly.CMvPolynomial.restrictTotalDegree d p = CPoly.CMvPolynomial.restrictBy (fun (m : CPoly.CMvMonomial n) => m.totalDegree ≤ d) p

def CPoly.CMvPolynomial.restrictDegree {n : ℕ} {R : Type} [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.

Equations

• CPoly.CMvPolynomial.restrictDegree d p = CPoly.CMvPolynomial.restrictBy (fun (m : CPoly.CMvMonomial n) => ∀ (i : Fin n), m.degreeOf i ≤ d) p