Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Matrix multiplication via auxiliary separation and polynomial multiplication

Theorem 1.1 gives a uniform arithmetic-operation bound for complex square matrix multiplication, and consequently an upper bound of 9/4 on its exponent. The two conclusions are stated separately in the existing arithmetic model.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.matrix_multiplication_cost_le line 21
Source documentation
Theorem 1.1: for every positive exponent slack, one constant bounds the cost of correct complex matrix multiplication programs at every positive size.
```
theorem matrix_multiplication_cost_le (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n →
      ∃ P : Arithmetic.MatrixAlgorithm ℂ n n n,
        P.Correct ∧ (P.cost : ℝ) ≤ C * (n : ℝ) ^ ((9 : ℝ) / 4 + ε) :=
…
```
Mentions: OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm
theorem OAI.MatrixMultiplication.AuxiliarySeparation.omega_le_nine_quarters line 28
Source documentation
The complex arithmetic matrix multiplication exponent is at most 9/4.
```
theorem omega_le_nine_quarters : Arithmetic.omega ℂ ≤ (9 : ℝ) / 4 :=
…
```
Mentions: OAI.MatrixMultiplication.Arithmetic.omega