OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCWPrimitiveDegeneration.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.outerMap_degree line 15
  2. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.middleMap_degree line 22
  3. def OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundary line 29
  4. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundary_basePolynomial line 45
  5. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.five_initial_coefficients line 48
  6. def OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundaryApproximation line 54
  7. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundaryApproximation_polynomial line 57
  8. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundaryApproximation_polynomial_apply line 63
  9. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundaryApproximation_leading line 84
  10. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.boundary_rank_power line 88
  11. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.cw_cyclic line 92
  12. def OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.cyclicBoundary line 98
  13. def OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.twiceCyclicBoundary line 113
  14. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.cyclicBoundary_deleted line 129
  15. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.twiceCyclicBoundary_deleted line 132
  16. def OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.cyclicBoundaryApproximation line 136
  17. def OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.twiceCyclicBoundaryApproximation line 140
  18. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.cyclicBoundaryApproximation_polynomial line 145
  19. theorem OAI.MatrixMultiplication.Foundation.CWPrimitiveDegeneration.twiceCyclicBoundaryApproximation_polynomial line 151