OAI/LinearAlgebra/MatrixMultiplication/Completion/RecursiveCompletion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. inductive OAI.MatrixMultiplication.Color line 17
  2. instance OAI.MatrixMultiplication.(instance at line 21) line 21
  3. structure OAI.MatrixMultiplication.FlaggedTensor line 25
  4. def OAI.MatrixMultiplication.RecursiveCompletion.raisedFlag line 36
  5. def OAI.MatrixMultiplication.RecursiveCompletion.flagB line 41
  6. def OAI.MatrixMultiplication.RecursiveCompletion.flagA line 44
  7. def OAI.MatrixMultiplication.RecursiveCompletion.flagC line 47
  8. def OAI.MatrixMultiplication.RecursiveCompletion.weight line 50
  9. theorem OAI.MatrixMultiplication.RecursiveCompletion.weight_pos line 56
  10. def OAI.MatrixMultiplication.RecursiveCompletion.complete line 101
  11. theorem OAI.MatrixMultiplication.RecursiveCompletion.complete_tensor line 114
  12. def OAI.MatrixMultiplication.RecursiveCompletion.diagonalMap line 119
  13. theorem OAI.MatrixMultiplication.RecursiveCompletion.restrict_diagonal line 122
  14. def OAI.MatrixMultiplication.RecursiveCompletion.flagPolynomial line 131
  15. theorem OAI.MatrixMultiplication.RecursiveCompletion.flagPolynomial_eq line 133
  16. theorem OAI.MatrixMultiplication.RecursiveCompletion.flagPolynomial_degree line 138
  17. def OAI.MatrixMultiplication.RecursiveCompletion.leftMap line 144
  18. def OAI.MatrixMultiplication.RecursiveCompletion.middleMap line 148
  19. def OAI.MatrixMultiplication.RecursiveCompletion.rightMap line 152
  20. theorem OAI.MatrixMultiplication.RecursiveCompletion.diagonalMap_flag_degree line 156
  21. theorem OAI.MatrixMultiplication.RecursiveCompletion.scalingPolynomial line 163
  22. def OAI.MatrixMultiplication.RecursiveCompletion.completionDegeneration line 174