OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/CW75ReorderedExecution.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. abbrev OAI.MatrixMultiplication.CW75ReorderedExecution.Position line 24
  2. abbrev OAI.MatrixMultiplication.CW75ReorderedExecution.Coordinate line 25
  3. abbrev OAI.MatrixMultiplication.CW75ReorderedExecution.Prefix line 26
  4. def OAI.MatrixMultiplication.CW75ReorderedExecution.readerPair line 29
  5. def OAI.MatrixMultiplication.CW75ReorderedExecution.pairingProduct line 34
  6. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.pairingProduct_zero line 38
  7. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.pairingProduct_succ line 41
  8. def OAI.MatrixMultiplication.CW75ReorderedExecution.prefixValue line 46
  9. structure OAI.MatrixMultiplication.CW75ReorderedExecution.Bundle line 54
  10. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.position_card line 83
  11. def OAI.MatrixMultiplication.CW75ReorderedExecution.initial line 87
  12. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.previous_eligible line 125
  13. def OAI.MatrixMultiplication.CW75ReorderedExecution.refinedExecution line 141
  14. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.refinedExecution_normal line 152
  15. def OAI.MatrixMultiplication.CW75ReorderedExecution.extendBundle line 206
  16. def OAI.MatrixMultiplication.CW75ReorderedExecution.extendXY line 259
  17. def OAI.MatrixMultiplication.CW75ReorderedExecution.extendXZ line 283
  18. def OAI.MatrixMultiplication.CW75ReorderedExecution.extendYZ line 307
  19. def OAI.MatrixMultiplication.CW75ReorderedExecution.realize line 333
  20. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.realize_dimensions line 341
  21. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.realize_rankBound line 361
  22. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.realize_volume line 365
  23. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.realize_pairing_budget line 371
  24. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.realize_value line 375
  25. theorem OAI.MatrixMultiplication.CW75ReorderedExecution.realize_label_card line 388