Slot layouts

A layout numbers the exponent vectors m with mᵢ < rᵢ by the mixed-radix index idx m = Σ mᵢ sᵢ < n. A polynomial whose exponents fit is the sum over the n slots of its coefficients at dig j, both at the Kronecker point tᵢ = 2^(W sᵢ) and anywhere else.

structure Cayley.Pack.Layout : Type

• r : Fin 5 → ℕ
• s : Fin 5 → ℕ
• n : ℕ

def Cayley.Pack.Layout.idx (L : Layout) (m : Fin 5 → ℕ) : ℕ

Equations

• L.idx m = m 0 * L.s 0 + m 1 * L.s 1 + m 2 * L.s 2 + m 3 * L.s 3 + m 4 * L.s 4

def Cayley.Pack.Layout.dig (L : Layout) (j : ℕ) (i : Fin 5) : ℕ

Equations

• L.dig j i = j / L.s i % L.r i

noncomputable def Cayley.Pack.Layout.digF (L : Layout) (j : ℕ) : Fin 5 →₀ ℕ

The exponent vector of slot j.

Equations

• L.digF j = Finsupp.equivFunOnFinite.symm (L.dig j)

structure Cayley.Pack.Layout.Good (L : Layout) : Prop

The mixed-radix facts, checked by decide for each concrete layout.

• idx_dig (j : ℕ) : j < L.n → L.idx (L.dig j) = j
• dig_idx (m : Fin 5 → ℕ) : (∀ (i : Fin 5), m i < L.r i) → L.idx m < L.n ∧ ∀ (i : Fin 5), L.dig (L.idx m) i = m i

def Cayley.Pack.Layout.evSlot (L : Layout) (j : ℕ) : Bool

Slot j is even when every exponent is even.

Equations

• L.evSlot j = (List.finRange 5).all fun (i : Fin 5) => L.dig j i % 2 == 0

theorem Cayley.Pack.Layout.sum_support_eq {L : Layout} {R : Type u_1} [AddCommMonoid R] (hL : L.Good) (p : MvPolynomial (Fin 5) ℤ) (hbox : ∀ m ∈ p.support, ∀ (i : Fin 5), m i < L.r i) (H : (Fin 5 →₀ ℕ) → ℤ → R) (H0 : ∀ (m : Fin 5 →₀ ℕ), H m 0 = 0) : ∑ m ∈ p.support, H m (p.coeff m) = ∑ j ∈ Finset.range L.n, H (L.digF j) (p.coeff (L.digF j))

noncomputable def Cayley.Pack.Layout.cf (L : Layout) (e : PE) (j : ℕ) : ℤ

Slot coefficients of a polynomial expression.

Equations

• L.cf e j = e.mv.coeff (L.digF j)

def Cayley.Pack.Layout.Fits (L : Layout) (e : PE) : Prop

Exponents fit the layout.

Equations

• L.Fits e = ∀ (i : Fin 5), Cayley.Pack.PE.deg i e < L.r i

theorem Cayley.Pack.Layout.fits_box {L : Layout} {e : PE} (h : L.Fits e) (m : Fin 5 →₀ ℕ) : m ∈ e.mv.support → ∀ (i : Fin 5), m i < L.r i

theorem Cayley.Pack.Layout.ev_eq_sum {L : Layout} {R : Type u_1} [CommRing R] (hL : L.Good) {e : PE} (h : L.Fits e) (v : Fin 5 → R) : PE.ev v e = ∑ j ∈ Finset.range L.n, ↑(L.cf e j) * ∏ i : Fin 5, v i ^ L.dig j i

theorem Cayley.Pack.Layout.ev_kron {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) (W : ℕ) : PE.ev (fun (i : Fin 5) => 2 ^ (W * L.s i)) e = ∑ j ∈ Finset.range L.n, L.cf e j * 2 ^ (W * j)

At the Kronecker point.

theorem Cayley.Pack.Layout.abs_cf_le {L : Layout} {e : PE} (j : ℕ) : |L.cf e j| ≤ ↑e.nrm

theorem Cayley.Pack.Layout.sum_abs_cf_le {L : Layout} (hL : L.Good) {e : PE} (h : L.Fits e) : ∑ j ∈ Finset.range L.n, |L.cf e j| ≤ ↑e.nrm