OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/FieldCW.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.FieldCW.zeroForm line 20
  2. def OAI.MatrixMultiplication.FieldCW.interiorForm line 22
  3. def OAI.MatrixMultiplication.FieldCW.lastForm line 25
  4. def OAI.MatrixMultiplication.FieldCW.interiorSum line 27
  5. def OAI.MatrixMultiplication.FieldCW.tensor line 29
  6. theorem OAI.MatrixMultiplication.FieldCW.interior_pair_sum line 39
  7. theorem OAI.MatrixMultiplication.FieldCW.tensor_zero_side line 70
  8. theorem OAI.MatrixMultiplication.FieldCW.tensor_cyclic line 90
  9. def OAI.MatrixMultiplication.FieldCW.form line 108
  10. def OAI.MatrixMultiplication.FieldCW.left line 110
  11. def OAI.MatrixMultiplication.FieldCW.other line 115
  12. def OAI.MatrixMultiplication.FieldCW.polynomial line 120
  13. theorem OAI.MatrixMultiplication.FieldCW.rank_bound line 123
  14. theorem OAI.MatrixMultiplication.FieldCW.polynomial_apply line 129
  15. theorem OAI.MatrixMultiplication.FieldCW.coeff_mul_two line 143
  16. theorem OAI.MatrixMultiplication.FieldCW.coeff_mul_three line 149
  17. theorem OAI.MatrixMultiplication.FieldCW.vanishes line 155
  18. theorem OAI.MatrixMultiplication.FieldCW.leading line 167
  19. def OAI.MatrixMultiplication.FieldCW.degreeBound line 179
  20. theorem OAI.MatrixMultiplication.FieldCW.degree_bound line 183
  21. def OAI.MatrixMultiplication.FieldCW.approximation line 195
  22. theorem OAI.MatrixMultiplication.FieldCW.rank_power line 203