OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationTrialCells.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Memory of the complete stored representation trial

The prepared data and sampled families stay resident during the stopped schedule. The schedule itself reuses storage across residue classes.

  1. def OAI.LowSpaceSubsetSum.RepresentationTrialCells.core line 20
  2. abbrev OAI.LowSpaceSubsetSum.RepresentationTrialCells.bare line 36
  3. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.core_value line 38
  4. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.bare_congr line 55
  5. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.core_cells line 71
  6. def OAI.LowSpaceSubsetSum.RepresentationTrialCells.middle line 94
  7. def OAI.LowSpaceSubsetSum.RepresentationTrialCells.last line 102
  8. def OAI.LowSpaceSubsetSum.RepresentationTrialCells.run line 116
  9. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.bare_run line 123
  10. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.value line 137
  11. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.schedule_raw line 156
  12. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.schedule_order line 174
  13. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.schedule_cells line 186
  14. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.middle_cells line 211
  15. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.last_cells line 219
  16. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.bound_sum line 231
  17. theorem OAI.LowSpaceSubsetSum.RepresentationTrialCells.cells line 234