Unlawful multivariate polynomials

This file defines the Unlawful type, which represents multivariate polynomials as a map from monomials to coefficients. Unlike Lawful, it does not enforce the absence of zero coefficients.

Main definitions

• CPoly.Unlawful n R: A map from CMvMonomial n to R, implemented using Std.ExtTreeMap.

def CPoly.Unlawful (n : ℕ) (R : Type) : Type

Polynomial in n variables with coefficients in R. Internally represented as a tree map from monomials to coefficients.

Equations

• CPoly.Unlawful n R = Std.ExtTreeMap (CPoly.CMvMonomial n) R compare

instance CPoly.instEmptyCollectionUnlawful {n : ℕ} {R : Type} : EmptyCollection (Unlawful n R)

Equations

• CPoly.instEmptyCollectionUnlawful = { emptyCollection := ∅ }

instance CPoly.instSingletonMonoRUnlawful {n : ℕ} {R : Type} : Singleton (MonoR n R) (Unlawful n R)

Equations

• CPoly.instSingletonMonoRUnlawful = inferInstanceAs (Singleton (CPoly.MonoR n R) (Std.ExtTreeMap (CPoly.CMvMonomial n) R compare))

instance CPoly.instInsertMonoRUnlawful {n : ℕ} {R : Type} : Insert (MonoR n R) (Unlawful n R)

Equations

• CPoly.instInsertMonoRUnlawful = inferInstanceAs (Insert (CPoly.MonoR n R) (Std.ExtTreeMap (CPoly.CMvMonomial n) R compare))

instance CPoly.instLawfulSingletonMonoRUnlawful {n : ℕ} {R : Type} : LawfulSingleton (MonoR n R) (Unlawful n R)

instance CPoly.instMembershipCMvMonomialUnlawful {n : ℕ} {R : Type} : Membership (CMvMonomial n) (Unlawful n R)

Equations

• CPoly.instMembershipCMvMonomialUnlawful = inferInstanceAs (Membership (CPoly.CMvMonomial n) (Std.ExtTreeMap (CPoly.CMvMonomial n) R compare))

@[instance 10000, defaultInstance 1000]

instance CPoly.instGetElemUnlawfulCMvMonomialMem {n : ℕ} {R : Type} : GetElem (Unlawful n R) (CMvMonomial n) R fun (lp : Unlawful n R) (m : CMvMonomial n) => m ∈ lp

Equations

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

instance CPoly.instGetElem?UnlawfulCMvMonomialMem {n : ℕ} {R : Type} : GetElem? (Unlawful n R) (CMvMonomial n) R fun (lp : Unlawful n R) (m : CMvMonomial n) => m ∈ lp

Equations

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

instance CPoly.instLawfulGetElemUnlawfulCMvMonomialMem {n : ℕ} {R : Type} : LawfulGetElem (Unlawful n R) (CMvMonomial n) R fun (lp : Unlawful n R) (m : CMvMonomial n) => m ∈ lp

theorem CPoly.Unlawful.ext_getElem? {n : ℕ} {R : Type} {t₁ t₂ : Unlawful n R} (h : ∀ (k : CMvMonomial n), t₁[k]? = t₂[k]?) : t₁ = t₂

theorem CPoly.Unlawful.ext_getElem?_iff {n : ℕ} {R : Type} {t₁ t₂ : Unlawful n R} : t₁ = t₂ ↔ ∀ (k : CMvMonomial n), t₁[k]? = t₂[k]?

def CPoly.Unlawful.ofList {n : ℕ} {R : Type} (l : List (CMvMonomial n × R)) : Unlawful n R

Construct an Unlawful polynomial from a list of monomial-coefficient pairs.

Equations

• CPoly.Unlawful.ofList l = Std.ExtTreeMap.ofList l compare

def CPoly.Unlawful.extend {n : ℕ} {R : Type} (n' : ℕ) (p : Unlawful n R) : Unlawful (max n n') R

Extend the number of variables by padding monomials with zeros.

Equations

• CPoly.Unlawful.extend n' p = CPoly.Unlawful.ofList ((List.map (CPoly.CMvMonomial.extend n') (Std.ExtTreeMap.keys p)).zip (Std.ExtTreeMap.values p))

@[reducible, inline]

abbrev CPoly.Unlawful.isNoZeroCoef {n : ℕ} {R : Type} [Zero R] (p : Unlawful n R) : Prop

Check if the polynomial has no zero coefficients.

Equations

• p.isNoZeroCoef = ∀ (m : CPoly.CMvMonomial n), p[m]? ≠ some 0

def CPoly.Unlawful.toFinset {n : ℕ} {R : Type} [DecidableEq R] (p : Unlawful n R) : Finset (CMvMonomial n × R)

Equations

• p.toFinset = (Std.ExtTreeMap.toList p).toFinset

@[reducible, inline]

abbrev CPoly.Unlawful.monomials {n : ℕ} {R : Type} (p : Unlawful n R) : List (CMvMonomial n)

The list of monomials present in the polynomial.

Equations

• p.monomials = Std.ExtTreeMap.keys p

@[simp]

theorem CPoly.Unlawful.mem_monomials {n : ℕ} {R : Type} {m : CMvMonomial n} {up : Unlawful n R} : m ∈ up.monomials ↔ m ∈ up

instance CPoly.Unlawful.instRepr {n : ℕ} {R : Type} [Repr R] : Repr (Unlawful n R)

Equations

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

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

Constant polynomial.

Equations

• CPoly.Unlawful.C c = if c = 0 then ∅ else CPoly.Unlawful.ofList [CPoly.MonoR.C c]

instance CPoly.Unlawful.instOfNatOfNatNat {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : OfNat (Unlawful n R) 0

Equations

• CPoly.Unlawful.instOfNatOfNatNat = { ofNat := CPoly.Unlawful.C 0 }

instance CPoly.Unlawful.instOfNatOfNatCastOfNeZeroNat {n : ℕ} {R : Type} {m : ℕ} [Zero R] [BEq R] [LawfulBEq R] [NatCast R] [NeZero m] : OfNat (Unlawful n R) m

Equations

• CPoly.Unlawful.instOfNatOfNatCastOfNeZeroNat = { ofNat := CPoly.Unlawful.C ↑m }

@[simp]

theorem CPoly.Unlawful.C_zero {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : C 0 = 0

@[simp]

theorem CPoly.Unlawful.C_zero' {n : ℕ} : C 0 = 0

@[simp]

theorem CPoly.Unlawful.zero_eq_zero {R : Type} [Zero R] : Zero.zero = 0

theorem CPoly.Unlawful.zero_eq_empty {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : 0 = ∅

@[simp]

theorem CPoly.Unlawful.not_mem_C_zero {n : ℕ} {x : CMvMonomial n} : x ∉ C 0

@[simp]

theorem CPoly.Unlawful.not_mem_zero {n : ℕ} {R : Type} [Zero R] {x : CMvMonomial n} [BEq R] [LawfulBEq R] : x ∉ 0

@[simp]

theorem CPoly.Unlawful.isNoZeroCoef_zero {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : isNoZeroCoef 0

def CPoly.Unlawful.add {n : ℕ} {R : Type} [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R

Pointwise addition of coefficients.

Equations

• p₁.add p₂ = Std.ExtTreeMap.mergeWith (fun (x : CPoly.CMvMonomial n) (c₁ c₂ : R) => c₁ + c₂) p₁ p₂

instance CPoly.Unlawful.instAdd {n : ℕ} {R : Type} [Add R] : Add (Unlawful n R)

Equations

• CPoly.Unlawful.instAdd = { add := CPoly.Unlawful.add }

theorem CPoly.Unlawful.grind_add_skip {n : ℕ} {R : Type} [Add R] {p₁ p₂ : Unlawful n R} : p₁ + p₂ = Std.ExtTreeMap.mergeWith (fun (x : CMvMonomial n) (c₁ c₂ : R) => c₁ + c₂) p₁ p₂

def CPoly.Unlawful.addMonoR {n : ℕ} {R : Type} [Add R] (p : Unlawful n R) (term : MonoR n R) : Unlawful n R

Add a single monomial-coefficient term to a polynomial.

Equations

• p.addMonoR term = p + CPoly.Unlawful.ofList [term]

def CPoly.Unlawful.mul₀ {n : ℕ} {R : Type} [Mul R] (t : MonoR n R) (p : Unlawful n R) : Unlawful n R

Multiply a polynomial by a single monomial term.

Equations

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

@[simp]

theorem CPoly.Unlawful.mul₀_zero {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Mul R] {t : MonoR n R} : mul₀ t 0 = 0

def CPoly.Unlawful.mul {n : ℕ} {R : Type} [Mul R] [Add R] [Zero R] [BEq R] [LawfulBEq R] (p₁ p₂ : Unlawful n R) : Unlawful n R

Polynomial multiplication using a nested fold (distributive law).

Equations

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

instance CPoly.Unlawful.instMulOfLawfulBEqOfAddOfZero {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Mul R] [Add R] [Zero R] : Mul (Unlawful n R)

Equations

• CPoly.Unlawful.instMulOfLawfulBEqOfAddOfZero = { mul := CPoly.Unlawful.mul }

def CPoly.Unlawful.neg {n : ℕ} {R : Type} [Neg R] (p : Unlawful n R) : Unlawful n R

Negation (negates all coefficients).

Equations

• p.neg = Std.ExtTreeMap.map (fun (x : CPoly.CMvMonomial n) (v : R) => -v) p

instance CPoly.Unlawful.instNeg {n : ℕ} {R : Type} [Neg R] : Neg (Unlawful n R)

Equations

• CPoly.Unlawful.instNeg = { neg := CPoly.Unlawful.neg }

def CPoly.Unlawful.sub {n : ℕ} {R : Type} [Neg R] [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R

Subtraction.

Equations

• p₁.sub p₂ = p₁.add (-p₂)

instance CPoly.Unlawful.instSubOfAdd {n : ℕ} {R : Type} [Neg R] [Add R] : Sub (Unlawful n R)

Equations

• CPoly.Unlawful.instSubOfAdd = { sub := CPoly.Unlawful.sub }

def CPoly.Unlawful.leadingTerm? {n : ℕ} {R : Type} : Unlawful n R → Option (MonoR n R)

Return the term with the lexicographically largest monomial.

Equations

• CPoly.Unlawful.leadingTerm? = Std.ExtTreeMap.maxEntry?

def CPoly.Unlawful.leadingMonomial? {n : ℕ} {R : Type} : Unlawful n R → Option (CMvMonomial n)

Return the lexicographically largest monomial.

Equations

• CPoly.Unlawful.leadingMonomial? = Option.map Prod.fst ∘ CPoly.Unlawful.leadingTerm?

instance CPoly.Unlawful.instDecidableEq {n : ℕ} {R : Type} [DecidableEq R] : DecidableEq (Unlawful n R)

Equations

• x.instDecidableEq y = if h : Std.ExtTreeMap.toList x = Std.ExtTreeMap.toList y then isTrue ⋯ else isFalse ⋯

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

Equations

• CPoly.Unlawful.coeff m p = p[m]?.getD 0

@[simp]

theorem CPoly.Unlawful.filter_get {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : (Std.ExtTreeMap.filter (fun (x : CMvMonomial n) (c : R) => c != v) a)[m]?.getD v = a[m]?.getD v

theorem CPoly.Unlawful.add_getD? {n : ℕ} {R : Type} [CommSemiring R] {m : CMvMonomial n} {p q : Unlawful n R} : (p.add q)[m]?.getD 0 = p[m]?.getD 0 + q[m]?.getD 0