Main.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic complexity bounds for square and rectangular matrix multiplication.

theorem OAI.MatrixMultiplication.complex_omega_le_nine_quarters line 14
Source documentation
The complex square matrix multiplication exponent is at most 9/4.
Distinct definitions of this name: ComparatorChallenges/MatrixMultiplication.lean:118 (same statement text; different proof or body). Qualify references as OAI.MatrixMultiplication.complex_omega_le_nine_quarters@path.
```
theorem complex_omega_le_nine_quarters :
    Arithmetic.omega ℂ ≤ (9 : ℝ) / 4 :=
…
```
Mentions: OAI.MatrixMultiplication.Arithmetic.omega
theorem OAI.MatrixMultiplication.complex_alpha_gt_93_div_200 line 19
Source documentation
The complex dual matrix multiplication exponent is greater than 0.465.
Distinct definitions of this name: ComparatorChallenges/MatrixMultiplication.lean:122 (same statement text; different proof or body). Qualify references as OAI.MatrixMultiplication.complex_alpha_gt_93_div_200@path.
```
theorem complex_alpha_gt_93_div_200 :
    (93 : ℝ) / 200 < Arithmetic.complexAlpha :=
…
```
Mentions: OAI.MatrixMultiplication.Arithmetic.complexAlpha
theorem OAI.MatrixMultiplication.complex_rectangular_omega_lt_523_div_250 line 25
Source documentation
Multiplication of n × n^0.709 by n^0.709 × n complex matrices has arithmetic exponent less than 2.092.
Distinct definitions of this name: ComparatorChallenges/MatrixMultiplication.lean:126 (same statement text; different proof or body). Qualify references as OAI.MatrixMultiplication.complex_rectangular_omega_lt_523_div_250@path.
```
theorem complex_rectangular_omega_lt_523_div_250 :
    Arithmetic.rectangularOmega ℂ ((709 : ℝ) / 1000) < (523 : ℝ) / 250 :=
…
```
Mentions: OAI.MatrixMultiplication.Arithmetic.rectangularOmega