OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCWBoundary.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.Foundation.CWBoundary.deleted line 14
  2. def OAI.MatrixMultiplication.Foundation.CWBoundary.tensor line 17
  3. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.tensor_deleted line 21
  4. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.tensor_preserves line 23
  5. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.deleted_rankAtMost line 26
  6. def OAI.MatrixMultiplication.Foundation.CWBoundary.diagonalMap line 41
  7. def OAI.MatrixMultiplication.Foundation.CWBoundary.outerWeight line 44
  8. def OAI.MatrixMultiplication.Foundation.CWBoundary.middleWeight line 46
  9. def OAI.MatrixMultiplication.Foundation.CWBoundary.outerMap line 48
  10. def OAI.MatrixMultiplication.Foundation.CWBoundary.middleMap line 50
  11. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.restrict_diagonal_apply line 52
  12. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.weight_on_support line 58
  13. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.scale_lifted_tensor line 66
  14. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.scaling_identity line 83
  15. def OAI.MatrixMultiplication.Foundation.CWBoundary.scalingPolynomial line 89
  16. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.scalingPolynomial_apply line 93
  17. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.scalingPolynomial_coeff line 97
  18. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.scalingPolynomial_leading line 105
  19. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.scalingPolynomial_degree line 109
  20. def OAI.MatrixMultiplication.Foundation.CWBoundary.normalizedCurve line 117
  21. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.normalizedCurve_restriction line 120
  22. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.degeneration line 137
  23. def OAI.MatrixMultiplication.Foundation.CWBoundary.weight line 159
  24. def OAI.MatrixMultiplication.Foundation.CWBoundary.polynomial line 163
  25. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.polynomial_rankAtMost line 167
  26. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.polynomial_apply line 170
  27. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.weighted_degree line 184
  28. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.polynomial_leading line 193
  29. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.polynomial_vanishes line 210
  30. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.polynomial_degree line 220
  31. def OAI.MatrixMultiplication.Foundation.CWBoundary.approximation line 230
  32. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.borderRankAtMost line 237
  33. theorem OAI.MatrixMultiplication.Foundation.CWBoundary.rank_power line 240