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

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin {F : Type u_1} [Field F] {Input : Type u_2} {n : ℕ} : (Fin n → Expression F Input) → Expression F Input

Build an arithmetic expression for a finite sum, with zero as the empty sum.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin x_2 = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.literal 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin_eval {F : Type u_1} [Field F] {Input : Type u_2} {n : ℕ} (f : Fin n → Expression F Input) (inputs : Input → F) : eval inputs (sumFin f) = ∑ i : Fin n, eval inputs (f i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin_cost {F : Type u_1} [Field F] {Input : Type u_2} {n : ℕ} (f : Fin n → Expression F Input) : (sumFin f).cost = ∑ i : Fin n, (f i).cost + n

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveEntry {F : Type u_1} [Field F] {a b c : ℕ} (i : Fin a) (k : Fin c) : Expression F (MatrixInput a b c)

The schoolbook dot-product expression for one matrix-product entry.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveEntry_eval {F : Type u_1} [Field F] {a b c : ℕ} (i : Fin a) (k : Fin c) (A : Matrix (Fin a) (Fin b) F) (B : Matrix (Fin b) (Fin c) F) : Expression.eval (matrixInputs A B) (naiveEntry i k) = ∑ j : Fin b, A i j * B j k

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveEntry_cost {F : Type u_1} [Field F] {a b c : ℕ} (i : Fin a) (k : Fin c) : (naiveEntry i k).cost = 2 * b

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm {F : Type u_1} [Field F] (a b c : ℕ) : MatrixAlgorithm F a b c

Compile all schoolbook dot products into one matrix multiplication program.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm_correct {F : Type u_1} [Field F] (a b c : ℕ) : (naiveAlgorithm a b c).Correct

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm_cost {F : Type u_1} [Field F] (a b c : ℕ) : (naiveAlgorithm a b c).cost = 2 * a * b * c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm_cost_le {F : Type u_1} [Field F] (a b c : ℕ) : (naiveAlgorithm a b c).cost ≤ 2 * a * b * c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_three {F : Type u_1} [Field F] : AdmissibleExponent F 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_nonempty {F : Type u_1} [Field F] : {τ : ℝ | AdmissibleExponent F τ}.Nonempty