OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationScalarDraws.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The nested prime draw at the actually stored widths

Equality witnesses transport only the seed types. The called sampler reads the three widths from the supplied integer array.

  1. abbrev OAI.LowSpaceSubsetSum.RepresentationScalarDraws.Seed line 16
  2. def OAI.LowSpaceSubsetSum.RepresentationScalarDraws.nested line 19
  3. def OAI.LowSpaceSubsetSum.RepresentationScalarDraws.transport line 22
  4. theorem OAI.LowSpaceSubsetSum.RepresentationScalarDraws.nested_transport line 24
  5. def OAI.LowSpaceSubsetSum.RepresentationScalarDraws.sourceWidths line 29
  6. theorem OAI.LowSpaceSubsetSum.RepresentationScalarDraws.widths_eq line 32
  7. def OAI.LowSpaceSubsetSum.RepresentationScalarDraws.draw line 39
  8. theorem OAI.LowSpaceSubsetSum.RepresentationScalarDraws.draw_value line 44
  9. theorem OAI.LowSpaceSubsetSum.RepresentationScalarDraws.draw_work line 54