def Hex.FpPoly.Enumeration.coeffLists (p : Nat) [ZMod64.Bounds p] : Nat → List (List (ZMod64 p))

All coefficient lists of length d, with entries ranging over ZMod64 p.

Equations

• One or more equations did not get rendered due to their size.
• Hex.FpPoly.Enumeration.coeffLists p 0 = [[]]

@[simp]

theorem Hex.FpPoly.Enumeration.coeffLists_zero {p : Nat} [ZMod64.Bounds p] : coeffLists p 0 = [[]]

There is exactly one coefficient list of length 0: the empty list. Base case of coeffLists.

@[simp]

theorem Hex.FpPoly.Enumeration.coeffLists_succ {p : Nat} [ZMod64.Bounds p] (d : Nat) : coeffLists p (d + 1) = List.flatMap (fun (c : ZMod64 p) => List.map (fun (coeffs : List (ZMod64 p)) => c :: coeffs) (coeffLists p d)) (ZMod64.values p)

Coefficient lists of length d + 1 prepend each ZMod64 p value to every length-d list. Recursive step of coeffLists.

theorem Hex.FpPoly.Enumeration.length_of_mem_coeffLists {p : Nat} [ZMod64.Bounds p] {d : Nat} {coeffs : List (ZMod64 p)} (hmem : coeffs ∈ coeffLists p d) : coeffs.length = d

Every list produced by coeffLists p d has length exactly d.

theorem Hex.FpPoly.Enumeration.mem_coeffLists_iff {p : Nat} [ZMod64.Bounds p] {d : Nat} {coeffs : List (ZMod64 p)} : coeffs ∈ coeffLists p d ↔ coeffs.length = d ∧ ∀ (c : ZMod64 p), c ∈ coeffs → c ∈ ZMod64.values p

Membership in coeffLists is exactly fixed length plus residue membership.

@[simp]

theorem Hex.FpPoly.Enumeration.coeffLists_length {p : Nat} [ZMod64.Bounds p] (d : Nat) : (coeffLists p d).length = p ^ d

The coefficient-list enumeration has exactly p ^ d entries.

theorem Hex.FpPoly.Enumeration.coeffLists_nodup {p : Nat} [ZMod64.Bounds p] (d : Nat) : (coeffLists p d).Nodup

The fixed-length coefficient-list enumeration has no duplicate lists.

def Hex.FpPoly.Enumeration.ofCoeffList {p : Nat} [ZMod64.Bounds p] (coeffs : List (ZMod64 p)) : FpPoly p

Turn a fixed coefficient list into an FpPoly.

Equations

• Hex.FpPoly.Enumeration.ofCoeffList coeffs = Hex.DensePoly.ofList coeffs

def Hex.FpPoly.Enumeration.polysBelowDegree (p : Nat) [ZMod64.Bounds p] (d : Nat) : List (FpPoly p)

All FpPoly p values whose degree is below d, represented by length-d coefficient lists.

Equations

• Hex.FpPoly.Enumeration.polysBelowDegree p d = List.map Hex.FpPoly.Enumeration.ofCoeffList (Hex.FpPoly.Enumeration.coeffLists p d)

theorem Hex.FpPoly.Enumeration.of_first_coeffs_eq_of_degree_getD_lt {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {d : Nat} (hdeg : DensePoly.natDegree f < d) : ofCoeffList (List.map (fun (i : Nat) => DensePoly.coeff f i) (List.range d)) = f

The polynomial built from its first d coefficients is the original polynomial when the original degree is below d.

theorem Hex.FpPoly.Enumeration.mem_polysBelowDegree_of_degree_getD_lt {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {d : Nat} (hdeg : DensePoly.natDegree f < d) : f ∈ polysBelowDegree p d

Every polynomial with degree below d appears in the bounded-degree list.

theorem Hex.FpPoly.Enumeration.degree_getD_lt_of_mem_polysBelowDegree {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {d : Nat} (hd : 0 < d) (hmem : f ∈ polysBelowDegree p d) : DensePoly.natDegree f < d

Every polynomial in the bounded-degree enumeration has degree below the bound, provided the bound is positive.

theorem Hex.FpPoly.Enumeration.mem_polysBelowDegree_iff_degree_getD_lt {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {d : Nat} (hd : 0 < d) : f ∈ polysBelowDegree p d ↔ DensePoly.natDegree f < d

Membership in the bounded-degree enumeration is exactly degree below the positive bound.

@[simp]

theorem Hex.FpPoly.Enumeration.mem_polysBelowDegree_succ_iff_degree_getD_lt {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {d : Nat} : f ∈ polysBelowDegree p (d + 1) ↔ DensePoly.natDegree f < d + 1

Successor-bound membership in the bounded-degree enumeration.

theorem Hex.FpPoly.Enumeration.polysBelowDegree_nodup {p : Nat} [ZMod64.Bounds p] (d : Nat) : (polysBelowDegree p d).Nodup

The bounded-degree polynomial enumeration has no duplicate polynomial values.

@[simp]

theorem Hex.FpPoly.Enumeration.polysBelowDegree_length {p : Nat} [ZMod64.Bounds p] (d : Nat) : (polysBelowDegree p d).length = p ^ d

There are exactly p ^ d entries in the bounded-degree polynomial enumeration.