OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCW75InitialExecution.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. abbrev OAI.MatrixMultiplication.Foundation.CW75InitialExecution.Word line 15
  2. abbrev OAI.MatrixMultiplication.Foundation.CW75InitialExecution.Blocks line 16
  3. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.fullSource line 18
  4. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.support line 21
  5. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.support_iff line 23
  6. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundaryPolynomial line 28
  7. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundaryNormalized line 31
  8. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundaryPolynomial_factor line 35
  9. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundaryPolynomial_vanishes line 44
  10. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundaryPolynomial_leading line 49
  11. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.completionPolynomial line 55
  12. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundary_one line 60
  13. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.boundarySource_one line 68
  14. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.retained_coefficient_one line 75
  15. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.completion_eq line 82
  16. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.source_mul_retained line 88
  17. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.leftBlock line 95
  18. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.middleBlock line 99
  19. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.rightBlock line 103
  20. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.blockKernel line 107
  21. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.blockKernel_factor line 109
  22. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.blockKernel_vanishes line 132
  23. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.blockKernel_leading line 146
  24. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.degree_product line 159
  25. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.degree_expanded_product line 170
  26. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.outerWeight_degree line 179
  27. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.middleWeight_degree line 183
  28. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.leftBlock_degree line 187
  29. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.middleBlock_degree line 193
  30. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.rightBlock_degree line 199
  31. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.auxiliary line 205
  32. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.auxiliary_rank line 207
  33. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.leftMap line 212
  34. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.middleMap line 215
  35. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.rightMap line 218
  36. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.value line 221
  37. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.kernel_eq line 225
  38. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.kernel_coefficients line 231
  39. def OAI.MatrixMultiplication.Foundation.CW75InitialExecution.execution line 258
  40. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.execution_value line 278
  41. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.value_ne_zero_iff line 280
  42. theorem OAI.MatrixMultiplication.Foundation.CW75InitialExecution.value_retained line 285