OAI/LinearAlgebra/MatrixMultiplication/Tensor/BaseTensorBudgets.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.BaseTwo.first line 17
  2. def OAI.MatrixMultiplication.BaseTwo.other line 20
  3. def OAI.MatrixMultiplication.BaseTwo.polynomial line 23
  4. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_rank line 26
  5. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_difference line 29
  6. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_apply line 38
  7. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_coeff line 44
  8. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_leading line 53
  9. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_vanishes line 58
  10. theorem OAI.MatrixMultiplication.BaseTwo.polynomial_degree line 64
  11. def OAI.MatrixMultiplication.BaseTwo.approximation line 68
  12. def OAI.MatrixMultiplication.BaseTwo.flagged line 75
  13. def OAI.MatrixMultiplication.BaseTwo.leafColor line 82
  14. theorem OAI.MatrixMultiplication.BaseTwo.leafColor_owner line 84
  15. def OAI.MatrixMultiplication.BaseTwo.powerApproximation line 90
  16. theorem OAI.MatrixMultiplication.BaseTwo.rank_power line 94
  17. theorem OAI.MatrixMultiplication.BaseTwo.borderRankAtMost line 98
  18. def OAI.MatrixMultiplication.BaseThree.polynomial line 105
  19. theorem OAI.MatrixMultiplication.BaseThree.polynomial_apply line 108
  20. theorem OAI.MatrixMultiplication.BaseThree.polynomial_leading line 115
  21. theorem OAI.MatrixMultiplication.BaseThree.polynomial_vanishes line 121
  22. theorem OAI.MatrixMultiplication.BaseThree.polynomial_degree line 128
  23. def OAI.MatrixMultiplication.BaseThree.approximation line 133
  24. def OAI.MatrixMultiplication.BaseThree.flagged line 140
  25. def OAI.MatrixMultiplication.BaseThree.leafColor line 147
  26. theorem OAI.MatrixMultiplication.BaseThree.leafColor_owner line 149
  27. def OAI.MatrixMultiplication.BaseThree.powerApproximation line 155
  28. theorem OAI.MatrixMultiplication.BaseThree.rank_power line 159
  29. theorem OAI.MatrixMultiplication.BaseThree.borderRankAtMost line 163