OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorParameterExecution.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Integer execution of the separator sizes and sample counts

A constant-state power loop and binary-log loop compute the prescribed sample size. Five multiplicative binomial loops and four integer ceiling divisions compute the actual family-array lengths.

  1. def OAI.LowSpaceSubsetSum.SeparatorParameterExecution.powerLoop line 18
  2. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.powerLoop_formula line 22
  3. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.three_power_bound line 30
  4. def OAI.LowSpaceSubsetSum.SeparatorParameterExecution.logBits line 35
  5. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.logBits_value line 40
  6. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.logBits_work line 45
  7. def OAI.LowSpaceSubsetSum.SeparatorParameterExecution.sample line 50
  8. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.sample_value line 54
  9. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.sample_work line 57
  10. def OAI.LowSpaceSubsetSum.SeparatorParameterExecution.families line 62
  11. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.families_value line 69
  12. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.families_work line 74
  13. structure OAI.LowSpaceSubsetSum.SeparatorParameterExecution.Data line 85
  14. def OAI.LowSpaceSubsetSum.SeparatorParameterExecution.run line 89
  15. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.size_value line 94
  16. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.counts_value line 97
  17. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.work line 101
  18. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.rounded_size line 107
  19. theorem OAI.LowSpaceSubsetSum.SeparatorParameterExecution.rounded_counts line 112