OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCWLocalConstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. abbrev OAI.MatrixMultiplication.Foundation.CWLocalConstruction.Site line 14
  2. theorem OAI.MatrixMultiplication.Foundation.CWLocalConstruction.site_card line 16
  3. def OAI.MatrixMultiplication.Foundation.CWLocalConstruction.siteEquiv line 19
  4. def OAI.MatrixMultiplication.Foundation.CWLocalConstruction.sourceApproximation line 22
  5. abbrev OAI.MatrixMultiplication.Foundation.CWLocalConstruction.CWPrimitive line 44
  6. def OAI.MatrixMultiplication.Foundation.CWLocalConstruction.word line 50
  7. structure OAI.MatrixMultiplication.Foundation.CWLocalConstruction.SourceCompatible line 53
  8. theorem OAI.MatrixMultiplication.Foundation.CWLocalConstruction.SourceCompatible.inputSupported line 70
  9. theorem OAI.MatrixMultiplication.Foundation.CWLocalConstruction.SourceCompatible.designatedCoefficients line 75
  10. theorem OAI.MatrixMultiplication.Foundation.CWLocalConstruction.SourceCompatible.grade_eq_word_iff line 82
  11. def OAI.MatrixMultiplication.Foundation.CWLocalConstruction.SourceCompatible.terminalApproximation line 102
  12. structure OAI.MatrixMultiplication.Foundation.CWLocalConstruction.Admissible line 115
  13. theorem OAI.MatrixMultiplication.Foundation.CWLocalConstruction.Admissible.rankBound_pos line 123