Complex arithmetic programs and asymptotic matrix multiplication costs.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate (Input : Type u_1) (Register : Type u_2) : Type (max u_1 u_2)

Complex gates are the field-generic gates specialized to the complex numbers.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate Input Register = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate ℂ Input Register

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.eval {Input : Type u_1} {Register : Type u_2} (inputs : Input → ℂ) (registers : Register → ℂ) : Gate Input Register → ℂ

Evaluate a complex gate using the shared arithmetic semantics.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.eval inputs registers = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval inputs registers

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.cost {Input : Type u_1} {Register : Type u_2} : Gate Input Register → ℕ

Count the arithmetic operation performed by a complex gate.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.cost = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.cost

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program (Input : Type u_1) (registers : ℕ) : Type u_1

Complex programs use the shared field-generic straight-line syntax.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program Input registers = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program ℂ Input registers

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.nil {Input : Type u_1} : Program Input 0

The empty complex program.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.nil = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.nil

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.step {Input : Type u_1} {r : ℕ} (p : Program Input r) (g : Gate Input (Fin r)) : Program Input (r + 1)

Append one gate to a complex program.

Equations

• p.step g = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.step p g

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval {Input : Type u_1} {r : ℕ} : Program Input r → (Input → ℂ) → Fin r → ℂ

Evaluate the registers of a complex program using the shared interpreter.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost {Input : Type u_1} {r : ℕ} : Program Input r → ℕ

Total arithmetic cost of a complex program.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.cost

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixInput (n : ℕ) : Type

Input entries for the two square matrices.

Equations

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

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.matrixInputs {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) : MatrixInput n → ℂ

Assemble the two square matrices in the shared input representation.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.matrixInputs A B = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.matrixInputs A B

@[reducible, inline]

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

Square complex matrix algorithms are a specialization of rectangular field algorithms.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm n = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm ℂ n n n

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.eval {n : ℕ} (P : MatrixAlgorithm n) (A B : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin n) (Fin n) ℂ

Evaluate the output matrix of a square complex algorithm.

Equations

• P.eval A B = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.eval P A B

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.Correct {n : ℕ} (P : MatrixAlgorithm n) : Prop

Correctness for every pair of square complex input matrices.

Equations

• P.Correct = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.Correct P

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.cost {n : ℕ} (P : MatrixAlgorithm n) : ℕ

Total arithmetic cost of a square complex matrix algorithm.

Equations

• P.cost = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.cost P

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm : MatrixAlgorithm 1

The shared one-multiplication scalar algorithm over the complex numbers.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.scalarAlgorithm ℂ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm_correct : scalarAlgorithm.Correct

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm_cost : scalarAlgorithm.cost = 1

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.AdmissibleExponent (exponent : ℝ) : Prop

Uniform complex arithmetic bounds with arbitrarily small positive exponent slack.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.AdmissibleExponent exponent = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent ℂ exponent

@[reducible, inline]

noncomputable abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.omega : ℝ

The field-generic matrix multiplication exponent specialized to the complex numbers.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.omega = MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega ℂ

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication (a b c : ℕ) : Tensor ℂ (Fin a × Fin b) (Fin b × Fin c) (Fin c × Fin a)

The coefficient tensor encoding rectangular matrix multiplication.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication a b c x y z = if x.2 = y.1 ∧ y.2 = z.1 ∧ z.2 = x.1 then 1 else 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_matching (a b c : ℕ) (i : Fin a) (j : Fin b) (k : Fin c) : matrixMultiplication a b c (i, j) (j, k) (k, i) = 1