def Hex.Matrix.Packed.dotNatImpl : List Nat → List Nat → Nat

dotNat as recursive equations, the compiled implementation.

Equations

• Hex.Matrix.Packed.dotNatImpl (a :: as) (b :: bs) = (a.mul b).add (Hex.Matrix.Packed.dotNatImpl as bs)
• Hex.Matrix.Packed.dotNatImpl x✝¹ x✝ = 0

noncomputable def Hex.Matrix.Packed.dotNat : List Nat → List Nat → Nat

The dot product of two natural-number lists, stopping at the shorter. List.rec is applied directly instead of recursive equations elaborated through List.brecOn, whose below tuple the kernel would build and project at every term; noncomputable only suppresses compilation, and dotNat_eq_impl gives the compiler the equation form.

Equations

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

@[simp]

theorem Hex.Matrix.Packed.dotNat_nil (l : List Nat) : dotNat [] l = 0

@[simp]

theorem Hex.Matrix.Packed.dotNat_cons_nil (a : Nat) (as : List Nat) : dotNat (a :: as) [] = 0

@[simp]

theorem Hex.Matrix.Packed.dotNat_nil_right (l : List Nat) : dotNat l [] = 0

@[simp]

theorem Hex.Matrix.Packed.dotNat_cons_cons (a b : Nat) (as bs : List Nat) : dotNat (a :: as) (b :: bs) = (a.mul b).add (dotNat as bs)

@[csimp]

theorem Hex.Matrix.Packed.dotNat_eq_impl : dotNat = dotNatImpl

def Hex.Matrix.Packed.packRow (W : Nat) : List Nat → Nat

A row packed into one number with W-bit slots: Σ aₖ · 2^(W·k).

Equations

• Hex.Matrix.Packed.packRow W [] = 0
• Hex.Matrix.Packed.packRow W (a :: as) = a.add ((Hex.Matrix.Packed.packRow W as).shiftLeft W)

def Hex.Matrix.Packed.packRows (W : Nat) : List (List Nat) → List Nat

The rows packed.

Equations

• Hex.Matrix.Packed.packRows W [] = []
• Hex.Matrix.Packed.packRows W (r :: rs) = Hex.Matrix.Packed.packRow W r :: Hex.Matrix.Packed.packRows W rs

def Hex.Matrix.Packed.packRevAux (W : Nat) : Nat → Nat → List Nat → Nat

Horner accumulation of k more slots from the front of a list, missing entries read as 0: after k steps from acc, the entries consumed sit in reverse order below acc.

Equations

• Hex.Matrix.Packed.packRevAux W 0 x✝¹ x✝ = x✝¹
• Hex.Matrix.Packed.packRevAux W k.succ x✝ [] = Hex.Matrix.Packed.packRevAux W k (x✝.shiftLeft W) []
• Hex.Matrix.Packed.packRevAux W k.succ x✝ (a :: as) = Hex.Matrix.Packed.packRevAux W k ((x✝.shiftLeft W).add a) as

def Hex.Matrix.Packed.packCol (W r : Nat) (c : List Nat) : Nat

A column of vt cut or zero-padded to r entries and packed in reverse order, in r steps.

Equations

• Hex.Matrix.Packed.packCol W r c = Hex.Matrix.Packed.packRevAux W r 0 c

def Hex.Matrix.Packed.packCols (W r : Nat) : List (List Nat) → List Nat

The columns packed.

Equations

• Hex.Matrix.Packed.packCols W r [] = []
• Hex.Matrix.Packed.packCols W r (r_1 :: rs) = Hex.Matrix.Packed.packCol W r r_1 :: Hex.Matrix.Packed.packCols W r rs

def Hex.Matrix.Packed.slot (W r p : Nat) : Nat

Slot r − 1 of p: bits W·(r − 1), …, W·r − 1.

Equations

• Hex.Matrix.Packed.slot W r p = (p.shiftRight (W.mul (r - 1))).land ((Nat.pow 2 W).sub 1)

def Hex.Matrix.Packed.dotPacked (W r pb pc : Nat) : Nat

The dot product of a packed row and a reverse-packed column of r entries.

Equations

• Hex.Matrix.Packed.dotPacked W r pb pc = Hex.Matrix.Packed.slot W r (pb.mul pc)

def Hex.Matrix.Packed.dotIntImpl : List Int → List Int → Int

dotInt as recursive equations, the compiled implementation.

Equations

• Hex.Matrix.Packed.dotIntImpl (a :: as) (b :: bs) = (a.mul b).add (Hex.Matrix.Packed.dotIntImpl as bs)
• Hex.Matrix.Packed.dotIntImpl x✝¹ x✝ = 0

noncomputable def Hex.Matrix.Packed.dotInt : List Int → List Int → Int

The dot product of two integer lists, stopping at the shorter; List.rec applied directly, as dotNat.

Equations

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

@[simp]

theorem Hex.Matrix.Packed.dotInt_nil (l : List Int) : dotInt [] l = 0

@[simp]

theorem Hex.Matrix.Packed.dotInt_cons_nil (a : Int) (as : List Int) : dotInt (a :: as) [] = 0

@[simp]

theorem Hex.Matrix.Packed.dotInt_nil_right (l : List Int) : dotInt l [] = 0

@[simp]

theorem Hex.Matrix.Packed.dotInt_cons_cons (a b : Int) (as bs : List Int) : dotInt (a :: as) (b :: bs) = (a.mul b).add (dotInt as bs)

@[csimp]

theorem Hex.Matrix.Packed.dotInt_eq_impl : dotInt = dotIntImpl

def Hex.Matrix.Packed.column (j : Nat) : List (List Int) → List Int

Column j of a row list: the specification of columns, not on the kernel path.

Equations

• Hex.Matrix.Packed.column j [] = []
• Hex.Matrix.Packed.column j (r :: rs) = r.getD j 0 :: Hex.Matrix.Packed.column j rs

def Hex.Matrix.Packed.consCols : List Int → List (List Int) → List (List Int)

A row prepended entrywise to a list of columns: entry j of the row goes on top of column j; a short row contributes 0s, and entries past the last column are dropped.

Equations

• Hex.Matrix.Packed.consCols (a :: as) (c :: cs) = (a :: c) :: Hex.Matrix.Packed.consCols as cs
• Hex.Matrix.Packed.consCols [] (c :: cs) = (0 :: c) :: Hex.Matrix.Packed.consCols [] cs
• Hex.Matrix.Packed.consCols x✝ [] = []

def Hex.Matrix.Packed.emptyCols : Nat → List (List Int)

m empty columns.

Equations

• Hex.Matrix.Packed.emptyCols 0 = []
• Hex.Matrix.Packed.emptyCols k.succ = [] :: Hex.Matrix.Packed.emptyCols k

def Hex.Matrix.Packed.columns (m : Nat) : List (List Int) → List (List Int)

The m columns of a row list, built in one pass over the rows: n · m list steps, against the n · m indexed reads of O(index) each that column would cost.

Equations

• Hex.Matrix.Packed.columns m [] = Hex.Matrix.Packed.emptyCols m
• Hex.Matrix.Packed.columns m (r :: rs) = Hex.Matrix.Packed.consCols r (Hex.Matrix.Packed.columns m rs)

def Hex.Matrix.Packed.posParts : List Int → List Nat

The nonnegative parts of a signed row.

Equations

• Hex.Matrix.Packed.posParts [] = []
• Hex.Matrix.Packed.posParts (a :: as) = a.toNat :: Hex.Matrix.Packed.posParts as

def Hex.Matrix.Packed.negParts : List Int → List Nat

The nonpositive parts of a signed row, negated.

Equations

• Hex.Matrix.Packed.negParts [] = []
• Hex.Matrix.Packed.negParts (a :: as) = a.neg.toNat :: Hex.Matrix.Packed.negParts as

def Hex.Matrix.Packed.allAbsLt (k : Nat) : List Int → Bool

Every entry has absolute value below k.

Equations

• Hex.Matrix.Packed.allAbsLt k [] = true
• Hex.Matrix.Packed.allAbsLt k (a :: as) = (a.natAbs.blt k && Hex.Matrix.Packed.allAbsLt k as)

def Hex.Matrix.Packed.allAbsLtRows (k : Nat) : List (List Int) → Bool

Every entry of every row has absolute value below k.

Equations

• Hex.Matrix.Packed.allAbsLtRows k [] = true
• Hex.Matrix.Packed.allAbsLtRows k (r :: rs) = (Hex.Matrix.Packed.allAbsLt k r && Hex.Matrix.Packed.allAbsLtRows k rs)

def Hex.Matrix.Packed.packCut (W r : Nat) (l : List Nat) : Nat

A list cut or zero-padded to r entries and packed in order.

Equations

• Hex.Matrix.Packed.packCut W r l = Hex.Matrix.Packed.packRow W (List.take r l ++ List.replicate (r - l.length) 0)

def Hex.Matrix.Packed.packSignedCut (W r : Nat) (t : List Int) : Nat × Nat

A signed row cut or zero-padded to r entries, packed as its two parts.

Equations

• Hex.Matrix.Packed.packSignedCut W r t = (Hex.Matrix.Packed.packCut W r (Hex.Matrix.Packed.posParts t), Hex.Matrix.Packed.packCut W r (Hex.Matrix.Packed.negParts t))

def Hex.Matrix.Packed.packSignedRows (W r : Nat) : List (List Int) → List (Nat × Nat)

The rows so packed.

Equations

• Hex.Matrix.Packed.packSignedRows W r [] = []
• Hex.Matrix.Packed.packSignedRows W r (r_1 :: rs) = Hex.Matrix.Packed.packSignedCut W r r_1 :: Hex.Matrix.Packed.packSignedRows W r rs

def Hex.Matrix.Packed.packSignedCol (W r : Nat) (c : List Int) : Nat × Nat

A signed column cut or zero-padded to r entries, reverse-packed as its two parts.

Equations

• Hex.Matrix.Packed.packSignedCol W r c = (Hex.Matrix.Packed.packCol W r (Hex.Matrix.Packed.posParts c), Hex.Matrix.Packed.packCol W r (Hex.Matrix.Packed.negParts c))

def Hex.Matrix.Packed.packSignedCols (W r : Nat) : List (List Int) → List (Nat × Nat)

The columns so packed.

Equations

• Hex.Matrix.Packed.packSignedCols W r [] = []
• Hex.Matrix.Packed.packSignedCols W r (r_1 :: rs) = Hex.Matrix.Packed.packSignedCol W r r_1 :: Hex.Matrix.Packed.packSignedCols W r rs

def Hex.Matrix.Packed.dotIntPacked (W r : Nat) (t c : Nat × Nat) : Int

(t⁺ − t⁻) · (c⁺ − c⁻) from the packed parts: four packed dot products.

Equations

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