OAI/LinearAlgebra/MatrixMultiplication/Completion/Execution.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. abbrev OAI.MatrixMultiplication.CompletionExecution.Position line 23
  2. abbrev OAI.MatrixMultiplication.CompletionExecution.Coordinate line 24
  3. abbrev OAI.MatrixMultiplication.CompletionExecution.Prefix line 25
  4. def OAI.MatrixMultiplication.CompletionExecution.support line 28
  5. def OAI.MatrixMultiplication.CompletionExecution.pairingProduct line 33
  6. theorem OAI.MatrixMultiplication.CompletionExecution.pairingProduct_zero line 37
  7. theorem OAI.MatrixMultiplication.CompletionExecution.pairingProduct_succ line 40
  8. def OAI.MatrixMultiplication.CompletionExecution.prefixValue line 45
  9. structure OAI.MatrixMultiplication.CompletionExecution.Bundle line 53
  10. theorem OAI.MatrixMultiplication.CompletionExecution.position_card line 82
  11. def OAI.MatrixMultiplication.CompletionExecution.scalarAuxiliary line 86
  12. theorem OAI.MatrixMultiplication.CompletionExecution.scalarAuxiliary_rank line 88
  13. def OAI.MatrixMultiplication.CompletionExecution.initial line 93
  14. theorem OAI.MatrixMultiplication.CompletionExecution.previous_eligible line 146
  15. def OAI.MatrixMultiplication.CompletionExecution.refinedExecution line 162
  16. theorem OAI.MatrixMultiplication.CompletionExecution.refinedExecution_normal line 173
  17. def OAI.MatrixMultiplication.CompletionExecution.extendBundle line 227
  18. def OAI.MatrixMultiplication.CompletionExecution.extendXY line 280
  19. def OAI.MatrixMultiplication.CompletionExecution.extendXZ line 303
  20. def OAI.MatrixMultiplication.CompletionExecution.extendYZ line 326
  21. def OAI.MatrixMultiplication.CompletionExecution.extend line 349
  22. def OAI.MatrixMultiplication.CompletionExecution.run line 360
  23. def OAI.MatrixMultiplication.CompletionExecution.realize line 364
  24. theorem OAI.MatrixMultiplication.CompletionExecution.realize_dimensions line 367
  25. theorem OAI.MatrixMultiplication.CompletionExecution.realize_rankBound line 386
  26. theorem OAI.MatrixMultiplication.CompletionExecution.realize_volume line 391
  27. theorem OAI.MatrixMultiplication.CompletionExecution.realize_label_card line 398