'Lawful' finite supports

This file defines the Lawful subtype, which consists of Unlawful polynomials where all stored coefficients are guaranteed to be non-zero. This provides a canonical representation (similar to Finsupp) and is the primary representation used for computable multivariate polynomials.

Main definitions

• CPoly.Lawful n R: The subtype of Unlawful n R with no zero coefficients.

def CPoly.Lawful (n : ℕ) (R : Type) [Zero R] : Type

The subtype of polynomials with no zero coefficients.

Equations

• CPoly.Lawful n R = { p : CPoly.Unlawful n R // p.isNoZeroCoef }

instance CPoly.instEmptyCol {n : ℕ} {R : Type} [Zero R] : EmptyCollection (Lawful n R)

Equations

• CPoly.instEmptyCol = { emptyCollection := ⟨∅, ⋯⟩ }

instance CPoly.instGetElemLawfulCMvMonomialMemUnlawfulValIsNoZeroCoef {n : ℕ} {R : Type} [Zero R] : GetElem (Lawful n R) (CMvMonomial n) R fun (lp : Lawful n R) (m : CMvMonomial n) => m ∈ ↑lp

Equations

• CPoly.instGetElemLawfulCMvMonomialMemUnlawfulValIsNoZeroCoef = { getElem := fun (lp : CPoly.Lawful n R) (m : CPoly.CMvMonomial n) (h : m ∈ ↑lp) => (↑lp)[m] }

instance CPoly.instGetElem?LawfulCMvMonomialMemUnlawfulValIsNoZeroCoef {n : ℕ} {R : Type} [Zero R] : GetElem? (Lawful n R) (CMvMonomial n) R fun (lp : Lawful n R) (m : CMvMonomial n) => m ∈ ↑lp

Equations

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

instance CPoly.instMembershipCMvMonomialLawful {n : ℕ} {R : Type} [Zero R] : Membership (CMvMonomial n) (Lawful n R)

Equations

• CPoly.instMembershipCMvMonomialLawful = { mem := fun (lp : CPoly.Lawful n R) (m : CPoly.CMvMonomial n) => m ∈ ↑lp }

instance CPoly.instLawfulGetElemLawfulCMvMonomialMem {n : ℕ} {R : Type} [Zero R] : LawfulGetElem (Lawful n R) (CMvMonomial n) R fun (lp : Lawful n R) (m : CMvMonomial n) => m ∈ lp

@[simp]

theorem CPoly.Lawful.getElem?_eq_val_getElem? {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {m : CMvMonomial n} : p[m]? = (↑p)[m]?

@[simp]

theorem CPoly.Lawful.mem_iff_cast {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {x : CMvMonomial n} : x ∈ ↑p ↔ x ∈ p

theorem CPoly.Lawful.mem_iff {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {x : CMvMonomial n} : x ∈ p ↔ ∃ (v : R), v ≠ 0 ∧ p[x]? = some v

@[simp]

theorem CPoly.Lawful.getElem?_ne_some_zero {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {m : CMvMonomial n} : p[m]? ≠ some 0

theorem CPoly.Lawful.getD_getElem?_ne_zero_of_mem {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {m : CMvMonomial n} (h : m ∈ p) : p[m]?.getD 0 ≠ 0

@[simp]

theorem CPoly.Lawful.getElem_eq_getElem {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {m : CMvMonomial n} (h : m ∈ p) : p[m] = (↑p)[m]

def CPoly.Lawful.fromUnlawful {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] (p : Unlawful n R) : Lawful n R

Convert an Unlawful polynomial to a Lawful one by filtering out zero coefficients.

Equations

• CPoly.Lawful.fromUnlawful p = ⟨Std.ExtTreeMap.filter (fun (x : CPoly.CMvMonomial n) (c : R) => c != 0) p, ⋯⟩

theorem CPoly.Lawful.grind_fromUnlawful_congr {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] {p₁ p₂ : Unlawful n R} (h : p₁ = p₂) : fromUnlawful p₁ = fromUnlawful p₂

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

Construct a constant polynomial.

Equations

• CPoly.Lawful.C c = ⟨CPoly.Unlawful.C c, ⋯⟩

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

Equations

• CPoly.Lawful.instOfNat_zero = { ofNat := CPoly.Lawful.C 0 }

theorem CPoly.Lawful.zero_def {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : Zero.zero = C 0

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

Equations

• CPoly.Lawful.instOfNat = { ofNat := CPoly.Lawful.C ↑m }

@[simp]

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

@[simp]

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

theorem CPoly.Lawful.zero_eq_zero {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : 0 = ⟨0, ⋯⟩

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

@[simp]

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

@[simp]

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

@[simp]

theorem CPoly.Lawful.cast_fromUnlawful {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} [BEq R] [LawfulBEq R] : ↑(fromUnlawful ↑p) = ↑p

def CPoly.Lawful.extend {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] (n' : ℕ) (p : Lawful n R) : Lawful (max n n') R

Extend the number of variables in a polynomial.

Equations

• CPoly.Lawful.extend n' p = CPoly.Lawful.fromUnlawful (CPoly.Unlawful.extend n' ↑p)

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

Addition of polynomials (results in a lawful polynomial).

Equations

• p₁.add p₂ = CPoly.Lawful.fromUnlawful (↑p₁ + ↑p₂)

instance CPoly.Lawful.instAdd {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Add R] : Add (Lawful n R)

Equations

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

theorem CPoly.Lawful.grind_add_skip {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Add R] {p₁ p₂ : Lawful n R} : p₁ + p₂ = fromUnlawful ((↑p₁).add ↑p₂)

theorem CPoly.Lawful.grind_add_skip_aggressive {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Add R] {p₁ p₂ : Lawful n R} : p₁ + p₂ = fromUnlawful (Std.ExtTreeMap.mergeWith (fun (x : CMvMonomial n) (c₁ c₂ : R) => c₁ + c₂) ↑p₁ ↑p₂)

Note to self: This goes too far.

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

Multiplication of polynomials (results in a lawful polynomial).

Equations

• p₁.mul p₂ = CPoly.Lawful.fromUnlawful (↑p₁ * ↑p₂)

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

Equations

• CPoly.Lawful.instMulOfAdd = { mul := CPoly.Lawful.mul }

def CPoly.Lawful.npow {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [NatCast R] [Add R] [Mul R] : ℕ → Lawful n R → Lawful n R

Polynomial exponentiation.

Equations

• CPoly.Lawful.npow Nat.zero x✝ = 1
• CPoly.Lawful.npow n_1.succ x✝ = CPoly.Lawful.npow n_1 x✝ * x✝

instance CPoly.Lawful.instNatPowOfNatCastOfAddOfMul {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [NatCast R] [Add R] [Mul R] : NatPow (Lawful n R)

Equations

• CPoly.Lawful.instNatPowOfNatCastOfAddOfMul = { pow := fun (e : CPoly.Lawful n R) (b : ℕ) => CPoly.Lawful.npow b e }

@[reducible, inline]

abbrev CPoly.Lawful.monomials {n : ℕ} {R : Type} [Zero R] (p : Lawful n R) : List (CMvMonomial n)

The list of monomials in a polynomial.

Equations

• p.monomials = (↑p).monomials

def CPoly.Lawful.NZConst {n : ℕ} {R : Type} [Zero R] (p : Lawful n R) : Prop

Check if a polynomial is a non-zero constant.

Equations

• p.NZConst = (Std.ExtTreeMap.size ↑p = 1 ∧ Std.ExtTreeMap.contains (↑p) CPoly.CMvMonomial.zero = true)

@[simp]

theorem CPoly.Lawful.mem_monomials_iff {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} {w : CMvMonomial n} : w ∈ p.monomials ↔ w ∈ p

instance CPoly.Lawful.instDecidableNZConst {n : ℕ} {R : Type} [Zero R] {p : Lawful n R} : Decidable p.NZConst

Equations

• CPoly.Lawful.instDecidableNZConst = id inferInstance

@[simp]

theorem CPoly.Lawful.fromUnlawful_cast {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] {p : Lawful n R} : fromUnlawful ↑p = p

def CPoly.Lawful.neg {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Neg R] (p : Lawful n R) : Lawful n R

Negation of a polynomial.

Equations

• p.neg = CPoly.Lawful.fromUnlawful (↑p).neg

instance CPoly.Lawful.instNeg {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Neg R] : Neg (Lawful n R)

Equations

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

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

Subtraction of polynomials.

Equations

• p₁.sub p₂ = p₁ + -p₂

instance CPoly.Lawful.instSubOfAddOfNeg {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [Add R] [Neg R] : Sub (Lawful n R)

Equations

• CPoly.Lawful.instSubOfAddOfNeg = { sub := CPoly.Lawful.sub }

instance CPoly.Lawful.instDecidableEq {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [DecidableEq R] : DecidableEq (Lawful n R)

Equations

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

def CPoly.Lawful.X (i : ℕ) : Lawful (i + 1) ℤ

The $i$-th variable as a polynomial.

Equations

• CPoly.Lawful.X i = CPoly.Lawful.fromUnlawful (CPoly.Unlawful.ofList [((Vector.replicate i 0).push 1, 1)])

def CPoly.Lawful.align {R : Type} [Zero R] [BEq R] [LawfulBEq R] {n₁ n₂ : ℕ} (p₁ : Lawful n₁ R) (p₂ : Lawful n₂ R) : Lawful (max n₁ n₂) R × Lawful (max n₁ n₂) R

Align two polynomials by extending them to have the same number of variables.

Equations

• p₁.align p₂ = (cast ⋯ (CPoly.Lawful.extend (max n₁ n₂) p₁), cast ⋯ (CPoly.Lawful.extend (max n₁ n₂) p₂))

def CPoly.Lawful.liftPoly {R : Type} [Zero R] [BEq R] [LawfulBEq R] {n₁ n₂ : ℕ} (f : Lawful (max n₁ n₂) R → Lawful (max n₁ n₂) R → Lawful (max n₁ n₂) R) (p₁ : Lawful n₁ R) (p₂ : Lawful n₂ R) : Lawful (max n₁ n₂) R

Lift a binary polynomial operation to handle polynomials with different numbers of variables.

Equations

• CPoly.Lawful.liftPoly f p₁ p₂ = Function.uncurry f (p₁.align p₂)

def CPoly.Lawful.polyCoe {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] (p : Lawful n R) : Lawful (n + 1) R

Equations

• p.polyCoe = cast ⋯ (CPoly.Lawful.extend n.succ p)

instance CPoly.Lawful.instCoeHAddNatOfNat {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : Coe (Lawful n R) (Lawful (n + 1) R)

Equations

• CPoly.Lawful.instCoeHAddNatOfNat = { coe := CPoly.Lawful.polyCoe }

@[instance 100]

instance CPoly.Lawful.instHAddMaxNatOfAdd {R : Type} [Zero R] [BEq R] [LawfulBEq R] {n₁ n₂ : ℕ} [Add R] : HAdd (Lawful n₁ R) (Lawful n₂ R) (Lawful (max n₁ n₂) R)

Equations

• CPoly.Lawful.instHAddMaxNatOfAdd = { hAdd := fun (p₁ : CPoly.Lawful n₁ R) (p₂ : CPoly.Lawful n₂ R) => CPoly.Lawful.liftPoly (fun (x1 x2 : CPoly.Lawful (max n₁ n₂) R) => x1 + x2) p₁ p₂ }

@[instance 100]

instance CPoly.Lawful.instHSubMaxNatOfAddOfNeg {R : Type} [Zero R] [BEq R] [LawfulBEq R] {n₁ n₂ : ℕ} [Add R] [Neg R] : HSub (Lawful n₁ R) (Lawful n₂ R) (Lawful (max n₁ n₂) R)

Equations

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

@[instance 100]

instance CPoly.Lawful.instHMulMaxNatOfAddOfMul {R : Type} [Zero R] [BEq R] [LawfulBEq R] {n₁ n₂ : ℕ} [Add R] [Mul R] : HMul (Lawful n₁ R) (Lawful n₂ R) (Lawful (max n₁ n₂) R)

Equations

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