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

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.registerCost {F : Type u_1} {Input : Type u_2} {r : ℕ} : Program F Input r → Fin r → ℕ

Charge each register only for the arithmetic operation that created it.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.nil.registerCost = Fin.elim0
• (p.step g).registerCost = fun (i : Fin (n + 1)) => Fin.cases g.cost p.registerCost i

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.sum_registerCost {F : Type u_1} {Input : Type u_2} {r : ℕ} (p : Program F Input r) : ∑ i : Fin r, p.registerCost i = p.cost

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_eq_constant_or_input_of_registerCost_eq_zero {F : Type u_1} {Input : Type u_2} [Field F] {r : ℕ} (p : Program F Input r) (i : Fin r) (hi : p.registerCost i = 0) : (∃ (z : F), ∀ (inputs : Input → F), p.eval inputs i = z) ∨ ∃ (a : Input), ∀ (inputs : Input → F), p.eval inputs i = inputs a

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.elementaryLeft {F : Type u_1} [Field F] {a b : ℕ} (i : Fin a) (j : Fin b) : Matrix (Fin a) (Fin b) F

A matrix unit for isolating a left-input entry in the arithmetic lower bound.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.elementaryLeft i j x y = if x = i then if y = j then 1 else 0 else 0

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.elementaryRight {F : Type u_1} [Field F] {b c : ℕ} (j : Fin b) (k : Fin c) : Matrix (Fin b) (Fin c) F

A matrix unit for isolating a right-input entry in the arithmetic lower bound.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.elementaryRight j k y z = if z = k then if y = j then 1 else 0 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.elementaryProduct {F : Type u_1} [Field F] {a b c : ℕ} (i x : Fin a) (j : Fin b) (k z : Fin c) : (elementaryLeft i j * elementaryRight j k) x z = if (x, z) = (i, k) then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.output_injective {F : Type u_1} [Field F] {a b c : ℕ} (P : MatrixAlgorithm F a b c) (hb : 1 ≤ b) (hP : P.Correct) : Function.Injective fun (o : Fin a × Fin c) => P.output o.1 o.2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.one_le_output_registerCost {F : Type u_1} [Field F] {a b c : ℕ} (P : MatrixAlgorithm F a b c) (hb : 1 ≤ b) (hP : P.Correct) (i : Fin a) (k : Fin c) : 1 ≤ P.program.registerCost (P.output i k)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.output_size_le_cost {F : Type u_1} [Field F] {a b c : ℕ} (P : MatrixAlgorithm F a b c) (hb : 1 ≤ b) (hP : P.Correct) : a * c ≤ P.cost

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_bddBelow (F : Type u_1) [Field F] (k : ℝ) : BddBelow {τ : ℝ | RectangularAdmissibleExponent F k τ}

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_iff_rectangular_one (F : Type u_1) [Field F] (τ : ℝ) : AdmissibleExponent F τ ↔ RectangularAdmissibleExponent F 1 τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_two_le {F : Type u_1} [Field F] {τ : ℝ} (hτ : AdmissibleExponent F τ) : 2 ≤ τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_bddBelow (F : Type u_1) [Field F] : BddBelow {τ : ℝ | AdmissibleExponent F τ}

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega_le_of_admissibleExponent {F : Type u_1} [Field F] {τ : ℝ} (hτ : AdmissibleExponent F τ) : omega F ≤ τ

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_one (F : Type u_1) [Field F] : rectangularOmega F 1 = omega F