Complex arithmetic programs and asymptotic matrix multiplication costs.

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin {Input : Type u_1} {n : ℕ} (f : Fin n → Expression Input) : Expression Input

Form a finite sum using the shared field-generic expression implementation.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin f = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin f

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry {n : ℕ} (i k : Fin n) : Expression (MatrixInput n)

The schoolbook dot-product expression, specialized from the generic implementation.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry i k = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveEntry i k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry_eval {n : ℕ} (i k : Fin n) (A B : Matrix (Fin n) (Fin n) ℂ) : Expression.eval (matrixInputs A B) (naiveEntry i k) = ∑ j : Fin n, A i j * B j k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry_cost {n : ℕ} (i k : Fin n) : (naiveEntry i k).cost = 2 * n

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm (n : ℕ) : MatrixAlgorithm n

Compile the schoolbook algorithm using the shared field-generic construction.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm n = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm n n n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_correct (n : ℕ) : (naiveAlgorithm n).Correct

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_cost (n : ℕ) : (naiveAlgorithm n).cost = 2 * n ^ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_cost_le (n : ℕ) : (naiveAlgorithm n).cost ≤ 2 * n ^ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_three : AdmissibleExponent 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_nonempty : {τ : ℝ | AdmissibleExponent τ}.Nonempty