theorem HexMatrixTheory.dotNat_eq_sum (a b : List ℕ) : Hex.Matrix.Packed.dotNat a b = ∑ i : Fin a.length, a[i] * b.getD (↑i) 0

theorem HexMatrixTheory.dotNat_eq_sum' (a b : List ℕ) (r : ℕ) (ha : a.length = r) : Hex.Matrix.Packed.dotNat a b = ∑ i : Fin r, a.getD (↑i) 0 * b.getD (↑i) 0

theorem HexMatrixTheory.packRow_eq_ofDigits (W : ℕ) (l : List ℕ) : Hex.Matrix.Packed.packRow W l = Nat.ofDigits (2 ^ W) l

def HexMatrixTheory.addLists : List ℕ → List ℕ → List ℕ

Pointwise sum, the shorter list padded with zeros.

Equations

• HexMatrixTheory.addLists (a :: as) (b :: bs) = (a + b) :: HexMatrixTheory.addLists as bs
• HexMatrixTheory.addLists [] x✝ = x✝
• HexMatrixTheory.addLists x✝ [] = x✝

theorem HexMatrixTheory.addLists_getD (l m : List ℕ) (t : ℕ) : (addLists l m).getD t 0 = l.getD t 0 + m.getD t 0

theorem HexMatrixTheory.ofDigits_addLists (B : ℕ) (l m : List ℕ) : Nat.ofDigits B (addLists l m) = Nat.ofDigits B l + Nat.ofDigits B m

theorem HexMatrixTheory.ofDigits_map_mul (B a : ℕ) (l : List ℕ) : Nat.ofDigits B (List.map (fun (x : ℕ) => a * x) l) = a * Nat.ofDigits B l

def HexMatrixTheory.conv : List ℕ → List ℕ → List ℕ

The coefficient list of the product of two coefficient lists.

Equations

• HexMatrixTheory.conv [] x✝ = []
• HexMatrixTheory.conv (a :: as) x✝ = HexMatrixTheory.addLists (List.map (fun (x : ℕ) => a * x) x✝) (0 :: HexMatrixTheory.conv as x✝)

theorem HexMatrixTheory.ofDigits_conv (B : ℕ) (l m : List ℕ) : Nat.ofDigits B (conv l m) = Nat.ofDigits B l * Nat.ofDigits B m

theorem HexMatrixTheory.map_mul_getD (a : ℕ) (m : List ℕ) (t : ℕ) : (List.map (fun (x : ℕ) => a * x) m).getD t 0 = a * m.getD t 0

theorem HexMatrixTheory.conv_getD (l m : List ℕ) (t : ℕ) : (conv l m).getD t 0 = ∑ i ∈ Finset.range (t + 1), l.getD i 0 * m.getD (t - i) 0

theorem HexMatrixTheory.conv_getD_le (M : ℕ) (l m : List ℕ) (hl : ∀ x ∈ l, x < M) (hm : ∀ x ∈ m, x < M) (t : ℕ) : (conv l m).getD t 0 ≤ l.length * (M * M)

theorem HexMatrixTheory.dotNat_eq_conv_reverse (b c : List ℕ) (r : ℕ) (hb : b.length = r) (hc : c.length = r) : Hex.Matrix.Packed.dotNat b c = (conv b c.reverse).getD (r - 1) 0

theorem HexMatrixTheory.ofDigits_digit (B : ℕ) (hB : 1 < B) (D : List ℕ) (hD : ∀ d ∈ D, d < B) (k : ℕ) : Nat.ofDigits B D / B ^ k % B = D.getD k 0

theorem HexMatrixTheory.dotPacked_eq (M W r : ℕ) (b c : List ℕ) (hb : b.length = r) (hc : c.length = r) (hbM : ∀ x ∈ b, x < M) (hcM : ∀ x ∈ c, x < M) (hW : r * (M * M) < 2 ^ W) : Hex.Matrix.Packed.dotPacked W r (Hex.Matrix.Packed.packRow W b) (Hex.Matrix.Packed.packRow W c.reverse) = Hex.Matrix.Packed.dotNat b c

theorem HexMatrixTheory.dotNat_pad (b c : List ℕ) (r : ℕ) (hb : b.length = r) : Hex.Matrix.Packed.dotNat b (List.take r c ++ List.replicate (r - c.length) 0) = Hex.Matrix.Packed.dotNat b c

theorem HexMatrixTheory.padded_length (r : ℕ) (c : List ℕ) : (List.take r c ++ List.replicate (r - c.length) 0).length = r

theorem HexMatrixTheory.padded_lt (M r : ℕ) (hM : 0 < M) (c : List ℕ) (hc : ∀ x ∈ c, x < M) (x : ℕ) : x ∈ List.take r c ++ List.replicate (r - c.length) 0 → x < M

theorem HexMatrixTheory.packRow_replicate_zero (W k : ℕ) : Hex.Matrix.Packed.packRow W (List.replicate k 0) = 0

theorem HexMatrixTheory.packRevAux_eq (W k acc : ℕ) (l : List ℕ) : Hex.Matrix.Packed.packRevAux W k acc l = acc * 2 ^ (W * k) + Hex.Matrix.Packed.packRow W (List.take k l ++ List.replicate (k - l.length) 0).reverse

theorem HexMatrixTheory.packCol_eq (W r : ℕ) (c : List ℕ) : Hex.Matrix.Packed.packCol W r c = Hex.Matrix.Packed.packRow W (List.take r c ++ List.replicate (r - c.length) 0).reverse

theorem HexMatrixTheory.dotInt_eq_sum (a b : List ℤ) (r : ℕ) (h : a.length ≤ r) : Hex.Matrix.Packed.dotInt a b = ∑ k : Fin r, a.getD (↑k) 0 * b.getD (↑k) 0

theorem HexMatrixTheory.column_length (j : ℕ) (A : List (List ℤ)) : (Hex.Matrix.Packed.column j A).length = A.length

theorem HexMatrixTheory.column_getD (j : ℕ) (A : List (List ℤ)) (k : ℕ) : (Hex.Matrix.Packed.column j A).getD k 0 = (A.getD k []).getD j 0

theorem HexMatrixTheory.emptyCols_length (m : ℕ) : (Hex.Matrix.Packed.emptyCols m).length = m

theorem HexMatrixTheory.emptyCols_getD (m l : ℕ) : (Hex.Matrix.Packed.emptyCols m).getD l [] = []

theorem HexMatrixTheory.consCols_length (r : List ℤ) (cs : List (List ℤ)) : (Hex.Matrix.Packed.consCols r cs).length = cs.length

theorem HexMatrixTheory.consCols_getD (r : List ℤ) (cs : List (List ℤ)) (l : ℕ) (hl : l < cs.length) : (Hex.Matrix.Packed.consCols r cs).getD l [] = r.getD l 0 :: cs.getD l []

theorem HexMatrixTheory.columns_length (m : ℕ) (A : List (List ℤ)) : (Hex.Matrix.Packed.columns m A).length = m

theorem HexMatrixTheory.columns_getD (m : ℕ) (A : List (List ℤ)) (l : ℕ) (hl : l < m) : (Hex.Matrix.Packed.columns m A).getD l [] = Hex.Matrix.Packed.column l A

theorem HexMatrixTheory.dotNat_comm (a b : List ℕ) : Hex.Matrix.Packed.dotNat a b = Hex.Matrix.Packed.dotNat b a

theorem HexMatrixTheory.dotNat_cut (a b : List ℕ) (r : ℕ) (hb : b.length = r) : Hex.Matrix.Packed.dotNat (List.take r a ++ List.replicate (r - a.length) 0) b = Hex.Matrix.Packed.dotNat a b

Cutting or zero-padding the first list to the length of the second changes nothing.

theorem HexMatrixTheory.posPart_length (l : List ℤ) : (Hex.Matrix.Packed.posParts l).length = l.length

theorem HexMatrixTheory.negPart_length (l : List ℤ) : (Hex.Matrix.Packed.negParts l).length = l.length

theorem HexMatrixTheory.allAbsLt_iff (k : ℕ) (l : List ℤ) : Hex.Matrix.Packed.allAbsLt k l = true ↔ ∀ x ∈ l, x.natAbs < k

theorem HexMatrixTheory.allAbsLtRows_iff (k : ℕ) (rs : List (List ℤ)) : Hex.Matrix.Packed.allAbsLtRows k rs = true ↔ ∀ r ∈ rs, ∀ x ∈ r, x.natAbs < k

theorem HexMatrixTheory.posPart_lt (k : ℕ) (l : List ℤ) (h : ∀ x ∈ l, x.natAbs < k) (x : ℕ) : x ∈ Hex.Matrix.Packed.posParts l → x < k

theorem HexMatrixTheory.negPart_lt (k : ℕ) (l : List ℤ) (h : ∀ x ∈ l, x.natAbs < k) (x : ℕ) : x ∈ Hex.Matrix.Packed.negParts l → x < k

theorem HexMatrixTheory.dotInt_parts (t c : List ℤ) : Hex.Matrix.Packed.dotInt t c = ↑(Hex.Matrix.Packed.dotNat (Hex.Matrix.Packed.posParts t) (Hex.Matrix.Packed.posParts c) + Hex.Matrix.Packed.dotNat (Hex.Matrix.Packed.negParts t) (Hex.Matrix.Packed.negParts c)) - ↑(Hex.Matrix.Packed.dotNat (Hex.Matrix.Packed.posParts t) (Hex.Matrix.Packed.negParts c) + Hex.Matrix.Packed.dotNat (Hex.Matrix.Packed.negParts t) (Hex.Matrix.Packed.posParts c))

A signed dot product as the four dot products of the parts.

theorem HexMatrixTheory.dotIntPacked_eq (W r k : ℕ) (t c : List ℤ) (hc : c.length = r) (ht : ∀ x ∈ t, x.natAbs < k) (hck : ∀ x ∈ c, x.natAbs < k) (hW : r * (k * k) < 2 ^ W) : Hex.Matrix.Packed.dotIntPacked W r (Hex.Matrix.Packed.packSignedCut W r t) (Hex.Matrix.Packed.packSignedCol W r c) = Hex.Matrix.Packed.dotInt t c

The packed signed dot product of a row (cut or padded to r) with a column of r entries, both with absolute values below k and r · k² < 2^W.

theorem HexMatrixTheory.mem_column (j : ℕ) (A : List (List ℤ)) (x : ℤ) (hx : x ∈ Hex.Matrix.Packed.column j A) : (∃ r ∈ A, x ∈ r) ∨ x = 0

theorem HexMatrixTheory.mem_columns (m : ℕ) (A : List (List ℤ)) (c : List ℤ) (hc : c ∈ Hex.Matrix.Packed.columns m A) : ∃ j < m, c = Hex.Matrix.Packed.column j A

theorem HexMatrixTheory.columns_bound (m k : ℕ) (hk : 0 < k) (P : List (List ℤ)) (hb : ∀ r ∈ P, ∀ x ∈ r, x.natAbs < k) (c : List ℤ) : c ∈ Hex.Matrix.Packed.columns m P → c.length = P.length ∧ ∀ x ∈ c, x.natAbs < k

The m columns of a matrix with entries below k > 0 in absolute value have as many entries as the matrix has rows, all below k.

theorem HexMatrixTheory.dotInt_eq_sum_right (a b : List ℤ) (r : ℕ) (hb : b.length = r) : Hex.Matrix.Packed.dotInt a b = ∑ l : Fin r, a.getD (↑l) 0 * b.getD (↑l) 0

theorem HexMatrixTheory.list_ext_getD (l₁ l₂ : List ℤ) (hlen : l₁.length = l₂.length) (h : ∀ j < l₁.length, l₁.getD j 0 = l₂.getD j 0) : l₁ = l₂