OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCoppersmithWinograd.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.tensor line 19
  2. def OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.first line 22
  3. def OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.other line 27
  4. def OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.polynomial line 32
  5. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.rank_bound line 35
  6. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.polynomial_apply line 38
  7. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.leading line 60
  8. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.vanishes line 64
  9. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.degree_bound line 71
  10. def OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.approximation line 75
  11. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.borderRankAtMost line 82
  12. theorem OAI.MatrixMultiplication.Foundation.CoppersmithWinograd.rank_power line 85