OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCW75Primitive.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. abbrev OAI.MatrixMultiplication.Foundation.CW75Primitive.Word line 16
  2. def OAI.MatrixMultiplication.Foundation.CW75Primitive.source line 18
  3. def OAI.MatrixMultiplication.Foundation.CW75Primitive.hasB line 20
  4. def OAI.MatrixMultiplication.Foundation.CW75Primitive.hasC line 22
  5. def OAI.MatrixMultiplication.Foundation.CW75Primitive.allA line 24
  6. def OAI.MatrixMultiplication.Foundation.CW75Primitive.retained line 26
  7. def OAI.MatrixMultiplication.Foundation.CW75Primitive.tensor line 28
  8. def OAI.MatrixMultiplication.Foundation.CW75Primitive.mixed line 31
  9. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.boundary_active line 34
  10. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.source_factors line 40
  11. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.allA_iff line 45
  12. def OAI.MatrixMultiplication.Foundation.CW75Primitive.leftMap line 51
  13. def OAI.MatrixMultiplication.Foundation.CW75Primitive.middleMap line 54
  14. def OAI.MatrixMultiplication.Foundation.CW75Primitive.rightMap line 57
  15. def OAI.MatrixMultiplication.Foundation.CW75Primitive.polynomial line 60
  16. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.polynomial_apply line 63
  17. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.polynomial_identity line 70
  18. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.polynomial_coeff line 78
  19. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.leftMap_degree line 85
  20. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.middleMap_degree line 89
  21. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.rightMap_degree line 93
  22. def OAI.MatrixMultiplication.Foundation.CW75Primitive.restriction line 96
  23. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.restriction_basePolynomial line 117
  24. def OAI.MatrixMultiplication.Foundation.CW75Primitive.sourceApproximation line 119
  25. def OAI.MatrixMultiplication.Foundation.CW75Primitive.approximation line 122
  26. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.approximation_polynomial line 125
  27. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.leading line 133
  28. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.borderRankAtMost line 136
  29. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.original_support line 138
  30. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.originalWords_decode line 149
  31. def OAI.MatrixMultiplication.Foundation.CW75Primitive.component line 155
  32. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.component_injective line 162
  33. def OAI.MatrixMultiplication.Foundation.CW75Primitive.listedWord line 171
  34. def OAI.MatrixMultiplication.Foundation.CW75Primitive.listedX line 174
  35. def OAI.MatrixMultiplication.Foundation.CW75Primitive.listedY line 175
  36. def OAI.MatrixMultiplication.Foundation.CW75Primitive.listedZ line 176
  37. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.tensor_on_triple line 178
  38. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.mem_triples_shape line 199
  39. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.tensor_on_enumeration line 205
  40. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.retained_coefficient_one line 211
  41. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.listed_coefficient_count line 217
  42. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.listedWords_injective line 230
  43. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.boundary_component_complete line 242
  44. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.term_mem_all line 255
  45. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.triple_mem line 258
  46. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.triples_nodup line 262
  47. theorem OAI.MatrixMultiplication.Foundation.CW75Primitive.support_exhausted line 265