OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPreparedBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Work and live storage of the counted prime preparation stages

  1. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.scale_power line 14
  2. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.scale_positive line 18
  3. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.nestedAtWidths_bounded line 21
  4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.extraAtWidth_bounded line 48
  5. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.preparation_work line 59
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.preparation_combine line 96
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.nestedPrepared_bounded line 123
  8. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.extraPrepared_bounded line 139