OAI/Combinatorics/LowSpaceSubsetSum/Counting/ScalarSamplerArrays.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Retaining the accepted scalar draws as fixed-size arrays

The prime-width arguments are stored integers. These routines copy only accepted values and retain the bounded rejection sampler's actual work.

  1. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.factors line 16
  2. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.nested line 18
  3. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.nested_value line 23
  4. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.nested_work line 29
  5. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.moduli line 36
  6. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.moduli_value line 39
  7. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.extra line 44
  8. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.extra_value line 49
  9. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.extra_work line 53
  10. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.residueCoupling line 62
  11. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.residueExecution line 65
  12. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.residueValues line 70
  13. def OAI.LowSpaceSubsetSum.ScalarSamplerArrays.residues line 73
  14. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.residues_value line 78
  15. theorem OAI.LowSpaceSubsetSum.ScalarSamplerArrays.residues_work line 83