OAI/LinearAlgebra/MatrixMultiplication/Recovery/FiniteSchedule.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. def OAI.MatrixMultiplication.FiniteSchedule.lotTick line 16
  2. theorem OAI.MatrixMultiplication.FiniteSchedule.lotTick_lt line 18
  3. def OAI.MatrixMultiplication.FiniteSchedule.stageActive line 25
  4. instance OAI.MatrixMultiplication.FiniteSchedule.(instance at line 28) line 28
  5. theorem OAI.MatrixMultiplication.FiniteSchedule.stageActive_iff_unique_lot line 31
  6. theorem OAI.MatrixMultiplication.FiniteSchedule.lot_active_at_its_tick line 47
  7. def OAI.MatrixMultiplication.FiniteSchedule.tickCapacity line 53
  8. theorem OAI.MatrixMultiplication.FiniteSchedule.tickCapacity_first line 58
  9. theorem OAI.MatrixMultiplication.FiniteSchedule.tickCapacity_second line 64
  10. theorem OAI.MatrixMultiplication.FiniteSchedule.tickCapacity_interior line 71
  11. theorem OAI.MatrixMultiplication.FiniteSchedule.tickCapacity_penultimate line 80
  12. theorem OAI.MatrixMultiplication.FiniteSchedule.tickCapacity_last line 86
  13. theorem OAI.MatrixMultiplication.FiniteSchedule.sum_tick_minima line 92
  14. theorem OAI.MatrixMultiplication.FiniteSchedule.finite_schedule_yield line 127
  15. theorem OAI.MatrixMultiplication.FiniteSchedule.fixed_lot_boundary_limit line 134