Matrix multiplication via auxiliary separation and polynomial multiplication

Theorem 1.1 gives a uniform arithmetic-operation bound for square matrix multiplication over an algebraically closed field K of any characteristic (in particular K = ℂ), and consequently an upper bound of 9/4 on its exponent. The two conclusions are stated separately in the existing arithmetic model.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.matrix_multiplication_cost_le {K : Type} [Field K] [IsAlgClosed K] (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∃ (P : Arithmetic.MatrixAlgorithm K n n n), P.Correct ∧ ↑P.cost ≤ C * ↑n ^ (9 / 4 + ε)

Theorem 1.1: for every positive exponent slack, one constant bounds the cost of correct matrix multiplication programs over K at every positive size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.omega_le_nine_quarters {K : Type} [Field K] [IsAlgClosed K] : Arithmetic.omega K ≤ 9 / 4

The arithmetic matrix multiplication exponent of an algebraically closed field is at most 9/4.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.complex_omega_le_nine_quarters : Arithmetic.omega ℂ ≤ 9 / 4

The complex case.