Complex arithmetic interfaces specialized from the shared field-generic implementation.

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.zeroPadMatrix {n : ℕ} (m : ℕ) (A : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin m) (Fin m) ℂ

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

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.zeroPadMatrix m A = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix m m A

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.zeroPadMatrix_castLE {n m : ℕ} (h : n ≤ m) (A : Matrix (Fin n) (Fin n) ℂ) (i j : Fin n) : zeroPadMatrix m A (Fin.castLE h i) (Fin.castLE h j) = A i j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.sum_fin_castLE_of_zero {n m : ℕ} (h : n ≤ m) (f : Fin m → ℂ) (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.Foundation.Arithmetic.zeroPadMatrix_mul {n m : ℕ} (h : n ≤ m) (A B : Matrix (Fin n) (Fin n) ℂ) (i k : Fin n) : (zeroPadMatrix m A * zeroPadMatrix m B) (Fin.castLE h i) (Fin.castLE h k) = (A * B) i k

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.padSource {n m : ℕ} : MatrixInput m → MatrixInput n ⊕ ℂ

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

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.padSource = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.padSource

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.padSource_eval {n m : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) : (fun (x : MatrixInput m) => Sum.elim (matrixInputs A B) id (padSource x)) = matrixInputs (zeroPadMatrix m A) (zeroPadMatrix m B)

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad {n m : ℕ} (h : n ≤ m) (P : MatrixAlgorithm m) : MatrixAlgorithm n

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

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad h P = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad h h h P

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad_correct {n m : ℕ} (h : n ≤ m) {P : MatrixAlgorithm m} (hP : P.Correct) : (pad h P).Correct

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad_cost_eq {n m : ℕ} (h : n ≤ m) (P : MatrixAlgorithm m) : (pad h P).cost = P.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.exists_restrict {n m : ℕ} (h : n ≤ m) (P : MatrixAlgorithm m) (hP : P.Correct) : ∃ (Q : MatrixAlgorithm n), Q.Correct ∧ Q.cost ≤ P.cost