OAI/LinearAlgebra/MatrixMultiplication/Rectangular/ASI.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix multiplication algorithms and their asymptotic exponents.

  1. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_rankAtMost line 22
  2. theorem OAI.MatrixMultiplication.Arithmetic.rectangular_rpow_omega_le_of_rankAtMost line 40
  3. theorem OAI.MatrixMultiplication.Arithmetic.rectangular_rpow_omega_le_of_rank_growth line 62
  4. theorem OAI.MatrixMultiplication.Arithmetic.equalRectangular_inequality line 103
  5. theorem OAI.MatrixMultiplication.Arithmetic.power_le_of_forall_pow_le_square_linear_mul_pow line 143
  6. theorem OAI.MatrixMultiplication.Arithmetic.equalRectangular_inequality_of_polynomialApproximation line 155
  7. theorem OAI.MatrixMultiplication.Arithmetic.equalRectangular_log_inequality_of_polynomialApproximation line 174
  8. theorem OAI.MatrixMultiplication.Arithmetic.equalSquare_inequality_of_polynomialApproximation line 191
  9. theorem OAI.MatrixMultiplication.Arithmetic.equalVolume_inequality_of_polynomialApproximation line 214