OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCW75LabelHierarchy.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. abbrev OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.Word line 15
  2. abbrev OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.BitWord line 16
  3. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.retainedWords line 18
  4. abbrev OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.Scalar line 21
  5. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.scalar_mem line 23
  6. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.scalar_card line 27
  7. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.letter line 32
  8. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.grade line 34
  9. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.x line 37
  10. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.y line 38
  11. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.z line 39
  12. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.coefficient_one line 41
  13. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.coefficient_ne_zero line 44
  14. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.grade_injective line 49
  15. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.coordinates_injective line 56
  16. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.support_exhausted line 61
  17. abbrev OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.ActualSupport line 67
  18. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.toActualSupport line 70
  19. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.toActualSupport_bijective line 73
  20. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.actualSupportEquiv line 81
  21. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.actualSupport_card line 84
  22. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.decode_original_grade line 88
  23. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.retained_actual line 92
  24. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.source_ne_zero line 98
  25. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.hasB_iff_not_hasC line 104
  26. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.outer line 115
  27. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bPositions line 117
  28. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.cPositions line 118
  29. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.aChoices line 119
  30. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bChoices line 120
  31. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bPositions_eq_zero_of_outer_false line 122
  32. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.cPositions_eq_zero_of_outer_true line 131
  33. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.outerX line 139
  34. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.outerY line 140
  35. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bPositionsX line 142
  36. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bPositionsZ line 143
  37. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.cPositionsY line 146
  38. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.cPositionsZ line 147
  39. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.aChoicesY line 150
  40. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.aChoicesZ line 152
  41. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bChoicesX line 154
  42. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bChoicesY line 155
  43. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.outerX_read line 158
  44. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.outerY_read line 160
  45. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bPositionsX_read line 163
  46. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bPositionsZ_read line 165
  47. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.cPositionsY_read line 178
  48. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.cPositionsZ_read line 180
  49. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.aChoicesY_read line 193
  50. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.aChoicesZ_read line 205
  51. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bChoicesX_read line 207
  52. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.bChoicesY_read line 209
  53. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.term_bits_injective line 219
  54. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.positionLabels_injective line 231
  55. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.Label line 243
  56. instance OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.labelFintype line 247
  57. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.labels line 250
  58. inductive OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.Side line 258
  59. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.firstSide line 262
  60. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.secondSide line 266
  61. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.originalCoordinate line 270
  62. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.firstReader line 275
  63. def OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.secondReader line 283
  64. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.firstReader_readable line 291
  65. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.secondReader_readable line 301
  66. theorem OAI.MatrixMultiplication.Foundation.CW75LabelHierarchy.completeRecord_injective line 311