'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.

@[implicit_reducible]

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

The subtype of polynomials with no zero coefficients.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

instance CPoly.instLawfulGetElemLawfulCMvMonomialMem {n : ℕ} {R : Type u_1} [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 u_1} [Zero R] {p : Lawful n R} {m : CMvMonomial n} : p[m]? = (↑p)[m]?

@[simp]

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

theorem CPoly.Lawful.mem_iff {n : ℕ} {R : Type u_1} [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 u_1} [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 u_1} [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 u_1} [Zero R] {p : Lawful n R} {m : CMvMonomial n} (h : m ∈ p) : p[m] = (↑p)[m]

def CPoly.Lawful.fromUnlawful {n : ℕ} {R : Type u_1} [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.

theorem CPoly.Lawful.grind_fromUnlawful_congr {n : ℕ} {R : Type u_1} [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 u_1} [Zero R] [BEq R] [LawfulBEq R] (c : R) : Lawful n R

Construct a constant polynomial.

@[instance_reducible]

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

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

@[instance_reducible]

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

@[simp]

theorem CPoly.Lawful.C_zero {n : ℕ} {R : Type u_1} [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 u_1} [Zero R] [BEq R] [LawfulBEq R] : 0 = ⟨0, ⋯⟩

theorem CPoly.Lawful.zero_eq_empty {n : ℕ} {R : Type u_1} [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 u_1} [Zero R] {x : CMvMonomial n} [BEq R] [LawfulBEq R] : x ∉ 0

@[simp]

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

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

Extend the number of variables in a polynomial.

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

Addition of polynomials (results in a lawful polynomial).

@[instance_reducible]

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

theorem CPoly.Lawful.grind_add_skip {n : ℕ} {R : Type u_1} [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 u_1} [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 u_1} [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).

@[instance_reducible]

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

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

Polynomial exponentiation via repeated multiplication. O(k) multiplications.

This is the specification; npowBySq is the efficient O(log k) implementation used by the NatPow instance once the equivalence with this naive form has been proven.

@[irreducible, inline, specialize #[]]

def CPoly.Lawful.npowBySq {n : ℕ} {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] [NatCast R] [Add R] [Mul R] (p : Lawful n R) : ℕ → Lawful n R

Polynomial exponentiation via repeated squaring. O(log k) multiplications instead of O(k).

For k > 0, computes p ^ k by recursing on k / 2:

• If k is even: (p ^ (k / 2))²
• If k is odd: p · (p ^ (k / 2))²

Equivalent to npow (see npowBySq_eq_npow).

@[instance_reducible]

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

@[reducible, inline]

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

The list of monomials in a polynomial.

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

Check if a polynomial is a non-zero constant.

@[simp]

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

@[instance_reducible]

instance CPoly.Lawful.instDecidableNzConst {n : ℕ} {R : Type u_1} [Zero R] {p : Lawful n R} : Decidable p.NzConst

@[simp]

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

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

Negation of a polynomial.

@[instance_reducible]

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

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

Subtraction of polynomials.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

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

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

The $i$-th variable as a polynomial.

def CPoly.Lawful.align {R : Type u_1} [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.

def CPoly.Lawful.liftPoly {R : Type u_1} [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.

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

@[instance_reducible]

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

@[instance_reducible, instance 100]

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

@[instance_reducible, instance 100]

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

@[instance_reducible, instance 100]

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