OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Priority.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.priorityPermutation line 15
  2. def OAI.MatrixMultiplication.AllFieldHistory.PriorityLexLE line 20
  3. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 24) line 24
  4. theorem OAI.MatrixMultiplication.AllFieldHistory.priorityPermutation_surjective line 28
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.priorityPermutation_order line 31
  6. def OAI.MatrixMultiplication.AllFieldHistory.stageBRepresentatives line 35
  7. def OAI.MatrixMultiplication.AllFieldHistory.readInPriority line 38
  8. def OAI.MatrixMultiplication.AllFieldHistory.stageBPriorityIndex line 40
  9. def OAI.MatrixMultiplication.AllFieldHistory.stageBPriority line 44
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.stageBPriority_finite_spec line 46
  11. theorem OAI.MatrixMultiplication.AllFieldHistory.stageBPriority_reads_representative line 53
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.stageBPriority_lex_first line 57
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.stageBPriority_233 line 63
  14. def OAI.MatrixMultiplication.AllFieldHistory.cPriorityIndex line 69
  15. def OAI.MatrixMultiplication.AllFieldHistory.stageCPriorityLabel line 72
  16. theorem OAI.MatrixMultiplication.AllFieldHistory.stageCPriorityLabel_at_part line 75
  17. theorem OAI.MatrixMultiplication.AllFieldHistory.stageCPriorityLabel_remaining_order line 79
  18. def OAI.MatrixMultiplication.AllFieldHistory.cPriority line 84
  19. theorem OAI.MatrixMultiplication.AllFieldHistory.cPriority_at_part line 87
  20. theorem OAI.MatrixMultiplication.AllFieldHistory.cPriority_at_part_two line 91
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.cPriority_remaining_order line 97
  22. def OAI.MatrixMultiplication.AllFieldHistory.Work.priority line 102
  23. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.priority_stageA line 107
  24. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.priority_stageB line 110
  25. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.priority_stageC line 114
  26. def OAI.MatrixMultiplication.AllFieldHistory.PlacedWork.physicalOrder line 118
  27. theorem OAI.MatrixMultiplication.AllFieldHistory.work_placement_for_order_unique line 121
  28. abbrev OAI.MatrixMultiplication.AllFieldHistory.CanonicalActive line 125
  29. abbrev OAI.MatrixMultiplication.AllFieldHistory.ActiveOrder line 128
  30. def OAI.MatrixMultiplication.AllFieldHistory.canonicalActiveEquivOrder line 131
  31. def OAI.MatrixMultiplication.AllFieldHistory.workAmount line 150
  32. def OAI.MatrixMultiplication.AllFieldHistory.activeAggregateCapacity line 153
  33. def OAI.MatrixMultiplication.AllFieldHistory.physicalTickCapacity line 158
  34. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalTickCapacity_eq_partition line 164
  35. theorem OAI.MatrixMultiplication.AllFieldHistory.physicalTickCapacity_eq_sixth line 174
  36. theorem OAI.MatrixMultiplication.AllFieldHistory.sum_physicalTick_minima line 181