Polynomial expressions

PE is a tiny syntax for integer polynomials in five variables. PE.ev evaluates it in any commutative ring; PE.mv is the polynomial itself. The syntactic degree PE.deg bounds every exponent of PE.mv, and PE.nrm bounds the sum of the absolute values of its coefficients.

inductive Cayley.Pack.PE : Type

• c (z : ℤ) : PE
• x (i : Fin 5) : PE
• add (a b : PE) : PE
• sub (a b : PE) : PE
• mul (a b : PE) : PE

def Cayley.Pack.PE.ev {R : Type u_1} [CommRing R] (v : Fin 5 → R) : PE → R

Evaluation in a commutative ring.

Equations

• Cayley.Pack.PE.ev v (Cayley.Pack.PE.c z) = ↑z
• Cayley.Pack.PE.ev v (Cayley.Pack.PE.x i) = v i
• Cayley.Pack.PE.ev v (a.add b) = Cayley.Pack.PE.ev v a + Cayley.Pack.PE.ev v b
• Cayley.Pack.PE.ev v (a.sub b) = Cayley.Pack.PE.ev v a - Cayley.Pack.PE.ev v b
• Cayley.Pack.PE.ev v (a.mul b) = Cayley.Pack.PE.ev v a * Cayley.Pack.PE.ev v b

noncomputable def Cayley.Pack.PE.mv (e : PE) : MvPolynomial (Fin 5) ℤ

The polynomial.

Equations

• e.mv = Cayley.Pack.PE.ev MvPolynomial.X e

def Cayley.Pack.PE.deg (i : Fin 5) : PE → ℕ

Syntactic degree in variable i.

Equations

• Cayley.Pack.PE.deg i (Cayley.Pack.PE.c z) = 0
• Cayley.Pack.PE.deg i (Cayley.Pack.PE.x i_1) = if i_1 = i then 1 else 0
• Cayley.Pack.PE.deg i (a.add b) = max (Cayley.Pack.PE.deg i a) (Cayley.Pack.PE.deg i b)
• Cayley.Pack.PE.deg i (a.sub b) = max (Cayley.Pack.PE.deg i a) (Cayley.Pack.PE.deg i b)
• Cayley.Pack.PE.deg i (a.mul b) = Cayley.Pack.PE.deg i a + Cayley.Pack.PE.deg i b

def Cayley.Pack.PE.nrm : PE → ℕ

A bound on the sum of absolute values of the coefficients.

Equations

• (Cayley.Pack.PE.c z).nrm = z.natAbs
• (Cayley.Pack.PE.x i).nrm = 1
• (a.add b).nrm = a.nrm + b.nrm
• (a.sub b).nrm = a.nrm + b.nrm
• (a.mul b).nrm = a.nrm * b.nrm

theorem Cayley.Pack.PE.mv_c (z : ℤ) : (c z).mv = MvPolynomial.C z

theorem Cayley.Pack.PE.mv_x (i : Fin 5) : (x i).mv = MvPolynomial.X i

theorem Cayley.Pack.PE.mv_add (a b : PE) : (a.add b).mv = a.mv + b.mv

theorem Cayley.Pack.PE.mv_sub (a b : PE) : (a.sub b).mv = a.mv - b.mv

theorem Cayley.Pack.PE.mv_mul (a b : PE) : (a.mul b).mv = a.mv * b.mv

theorem Cayley.Pack.PE.ev_eq_eval₂ {R : Type u_1} [CommRing R] (v : Fin 5 → R) (e : PE) : ev v e = (MvPolynomial.eval₂Hom (Int.castRingHom R) v) e.mv

Evaluation is evaluation of the polynomial.

theorem Cayley.Pack.PE.support_deg (e : PE) (m : Fin 5 →₀ ℕ) : m ∈ e.mv.support → ∀ (i : Fin 5), m i ≤ deg i e

The ℓ¹ norm of the coefficients

noncomputable def Cayley.Pack.PE.l1 (p : MvPolynomial (Fin 5) ℤ) : ℤ

Σ |coeff|.

Equations

• Cayley.Pack.PE.l1 p = ∑ m ∈ p.support, |p.coeff m|

theorem Cayley.Pack.PE.l1_eq_of_subset {p : MvPolynomial (Fin 5) ℤ} {s : Finset (Fin 5 →₀ ℕ)} (h : p.support ⊆ s) : l1 p = ∑ m ∈ s, |p.coeff m|

theorem Cayley.Pack.PE.l1_add_le (p q : MvPolynomial (Fin 5) ℤ) : l1 (p + q) ≤ l1 p + l1 q

theorem Cayley.Pack.PE.l1_neg (p : MvPolynomial (Fin 5) ℤ) : l1 (-p) = l1 p

theorem Cayley.Pack.PE.l1_sub_le (p q : MvPolynomial (Fin 5) ℤ) : l1 (p - q) ≤ l1 p + l1 q

theorem Cayley.Pack.PE.l1_monomial (a : Fin 5 →₀ ℕ) (z : ℤ) : l1 ((MvPolynomial.monomial a) z) = |z|

theorem Cayley.Pack.PE.l1_sum_le {ι : Type u_1} (s : Finset ι) (f : ι → MvPolynomial (Fin 5) ℤ) : l1 (∑ i ∈ s, f i) ≤ ∑ i ∈ s, l1 (f i)

theorem Cayley.Pack.PE.l1_mul_le (p q : MvPolynomial (Fin 5) ℤ) : l1 (p * q) ≤ l1 p * l1 q

theorem Cayley.Pack.PE.l1_le_nrm (e : PE) : l1 e.mv ≤ ↑e.nrm

theorem Cayley.Pack.PE.abs_coeff_le_l1 (p : MvPolynomial (Fin 5) ℤ) (m : Fin 5 →₀ ℕ) : |p.coeff m| ≤ l1 p