OAI/Combinatorics/LowSpaceSubsetSum/Counting/MixerParameterExecution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Integer mixer parameter arithmetic after the measured counts

The count logarithms are computed by bounded division loops. Sorting and all four prime-width formulas then use only stored integers.

  1. def OAI.LowSpaceSubsetSum.MixerParameterExecution.low line 16
  2. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.low_value line 20
  3. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.low_work line 24
  4. structure OAI.LowSpaceSubsetSum.MixerParameterExecution.Parameters line 29
  5. def OAI.LowSpaceSubsetSum.MixerParameterExecution.run line 34
  6. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.order_value line 42
  7. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.low_values line 46
  8. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.low_values_of_counts line 53
  9. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.widths_value line 64
  10. theorem OAI.LowSpaceSubsetSum.MixerParameterExecution.work line 70