OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationResidueDraws.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Three bounded residue draws at the stored integer moduli

  1. def OAI.LowSpaceSubsetSum.RepresentationResidueDraws.Seed line 12
  2. def OAI.LowSpaceSubsetSum.RepresentationResidueDraws.run line 18
  3. def OAI.LowSpaceSubsetSum.RepresentationResidueDraws.transport line 25
  4. theorem OAI.LowSpaceSubsetSum.RepresentationResidueDraws.run_transport line 30
  5. def OAI.LowSpaceSubsetSum.RepresentationResidueDraws.sourceModuli line 36
  6. theorem OAI.LowSpaceSubsetSum.RepresentationResidueDraws.sourcePos line 38
  7. theorem OAI.LowSpaceSubsetSum.RepresentationResidueDraws.moduli_eq line 42
  8. def OAI.LowSpaceSubsetSum.RepresentationResidueDraws.draw line 48
  9. theorem OAI.LowSpaceSubsetSum.RepresentationResidueDraws.draw_value line 54
  10. theorem OAI.LowSpaceSubsetSum.RepresentationResidueDraws.draw_work line 66