OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationParameterPreparation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual mixer preparation supplies all four prime widths

Only the stored input and permutation are computational arguments. The sign set is needed solely to identify the result with the sampling experiment.

  1. def OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.run line 17
  2. theorem OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.counts_bound line 23
  3. theorem OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.order_formula line 31
  4. theorem OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.order_value line 40
  5. theorem OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.low_value line 47
  6. theorem OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.widths_value line 66
  7. theorem OAI.LowSpaceSubsetSum.RepresentationParameterPreparation.work line 85