OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Schedule.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.initialAncestor line 15
  2. def OAI.MatrixMultiplication.AllFieldHistory.ancestrySplits line 22
  3. def OAI.MatrixMultiplication.AllFieldHistory.ancestrySubdivisions line 31
  4. def OAI.MatrixMultiplication.AllFieldHistory.historyKey line 36
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.placement_preserved line 43
  6. inductive OAI.MatrixMultiplication.AllFieldHistory.Work line 47
  7. def OAI.MatrixMultiplication.AllFieldHistory.Work.source line 53
  8. def OAI.MatrixMultiplication.AllFieldHistory.Work.stage line 58
  9. def OAI.MatrixMultiplication.AllFieldHistory.Work.lot line 63
  10. def OAI.MatrixMultiplication.AllFieldHistory.Work.halfLength line 65
  11. def OAI.MatrixMultiplication.AllFieldHistory.Work.parentShape line 70
  12. def OAI.MatrixMultiplication.AllFieldHistory.Work.Branch line 75
  13. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 80) line 80
  14. def OAI.MatrixMultiplication.AllFieldHistory.Work.child line 83
  15. def OAI.MatrixMultiplication.AllFieldHistory.Work.splitShape line 89
  16. abbrev OAI.MatrixMultiplication.AllFieldHistory.PlacedWork line 95
  17. abbrev OAI.MatrixMultiplication.AllFieldHistory.Active line 96
  18. theorem OAI.MatrixMultiplication.AllFieldHistory.active_tick_lt line 99
  19. def OAI.MatrixMultiplication.AllFieldHistory.branchPopulation line 103
  20. theorem OAI.MatrixMultiplication.AllFieldHistory.branchPopulation_half line 107
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.branchPopulation_sum line 120
  22. def OAI.MatrixMultiplication.AllFieldHistory.terminal line 130
  23. def OAI.MatrixMultiplication.AllFieldHistory.resident line 137
  24. abbrev OAI.MatrixMultiplication.AllFieldHistory.State line 145
  25. theorem OAI.MatrixMultiplication.AllFieldHistory.terminal_carries line 147
  26. theorem OAI.MatrixMultiplication.AllFieldHistory.work_source_resident line 156
  27. theorem OAI.MatrixMultiplication.AllFieldHistory.a_child_resident line 166
  28. theorem OAI.MatrixMultiplication.AllFieldHistory.c_child_resident line 170