Division-free arithmetic programs over a field and their operation counts.

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix {F : Type u_1} [Field F] {a b : ℕ} (A B : ℕ) (M : Matrix (Fin a) (Fin b) F) : Matrix (Fin A) (Fin B) F

Embed a smaller matrix in a larger rectangle by filling the remaining entries with zero.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix A B M i j = if hi : ↑i < a then if hj : ↑j < b then M ⟨↑i, hi⟩ ⟨↑j, hj⟩ else 0 else 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix_castLE {F : Type u_1} [Field F] {a b A B : ℕ} (ha : a ≤ A) (hb : b ≤ B) (M : Matrix (Fin a) (Fin b) F) (i : Fin a) (j : Fin b) : zeroPadMatrix A B M (Fin.castLE ha i) (Fin.castLE hb j) = M i j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.sum_fin_castLE_of_zero {F : Type u_1} [Field F] {n m : ℕ} (h : n ≤ m) (f : Fin m → F) (hf : ∀ (j : Fin m), n ≤ ↑j → f j = 0) : ∑ j : Fin m, f j = ∑ j : Fin n, f (Fin.castLE h j)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix_mul {F : Type u_1} [Field F] {a b c A B C : ℕ} (ha : a ≤ A) (hb : b ≤ B) (hc : c ≤ C) (M : Matrix (Fin a) (Fin b) F) (N : Matrix (Fin b) (Fin c) F) (i : Fin a) (k : Fin c) : (zeroPadMatrix A B M * zeroPadMatrix B C N) (Fin.castLE ha i) (Fin.castLE hc k) = (M * N) i k

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.padSource {F : Type u_1} [Field F] {a b c A B C : ℕ} : MatrixInput A B C → MatrixInput a b c ⊕ F

Route a padded input position to its original entry or the scalar zero.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.padSource_eval {F : Type u_1} [Field F] {a b c A B C : ℕ} (M : Matrix (Fin a) (Fin b) F) (N : Matrix (Fin b) (Fin c) F) : (fun (x : MatrixInput A B C) => Sum.elim (matrixInputs M N) id (padSource x)) = matrixInputs (zeroPadMatrix A B M) (zeroPadMatrix B C N)

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad {F : Type u_1} [Field F] {a b c A B C : ℕ} (ha : a ≤ A) (_hb : b ≤ B) (hc : c ≤ C) (P : MatrixAlgorithm F A B C) : MatrixAlgorithm F a b c

Run a larger matrix algorithm on zero-padded inputs and retain the requested outputs.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad_correct {F : Type u_1} [Field F] {a b c A B C : ℕ} (ha : a ≤ A) (hb : b ≤ B) (hc : c ≤ C) {P : MatrixAlgorithm F A B C} (hP : P.Correct) : (pad ha hb hc P).Correct

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad_cost_eq {F : Type u_1} [Field F] {a b c A B C : ℕ} (ha : a ≤ A) (hb : b ≤ B) (hc : c ≤ C) (P : MatrixAlgorithm F A B C) : (pad ha hb hc P).cost = P.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.exists_restrict {F : Type u_1} [Field F] {a b c A B C : ℕ} (ha : a ≤ A) (hb : b ≤ B) (hc : c ≤ C) (P : MatrixAlgorithm F A B C) (hP : P.Correct) : ∃ (Q : MatrixAlgorithm F a b c), Q.Correct ∧ Q.cost ≤ P.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent.mono_aspect {F : Type u_1} [Field F] {k l τ : ℝ} (h : RectangularAdmissibleExponent F l τ) (hkl : k ≤ l) : RectangularAdmissibleExponent F k τ