OAI/Combinatorics/LowSpaceSubsetSum/Word/WordMeasuredBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

All-execution bounds including word sampling and retained seeds

  1. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.add_work line 16
  2. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.add_work_input line 26
  3. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.sampled line 29
  4. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.sampled_501 line 61
  5. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.compression line 78
  6. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.representation line 102
  7. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.round line 117
  8. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.repetition_work line 145
  9. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.repeated_work line 158
  10. theorem OAI.LowSpaceSubsetSum.WordMeasuredBounds.repeated_cells line 171