OAI/LinearAlgebra/MatrixMultiplication/Rectangular/ComplexASI.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix multiplication algorithms and their asymptotic exponents.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.rectangularTagEquiv line 14
  2. def OAI.MatrixMultiplication.Foundation.Tensor.rectangularIndexEquiv line 18
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_directSum_symmetrized_rank line 22
  4. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficients_directSum_of_injective line 31
  5. def OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixMultiplication_directSum_symmetrized line 49
  6. theorem OAI.MatrixMultiplication.Foundation.mul_rpow_third_le_of_cube line 62
  7. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.equalRectangular_inequality line 73
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.equalRectangular_inequality_of_polynomialApproximation line 84