OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPreparedPrimes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Prime draws from the counted layout preparation

The widths passed to the sampler are stored integers returned by the mixer counting procedure. Equalities with ideal parameters are type transports.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.nested_width line 18
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.nestedAtWidths line 28
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.nestedFromPrepared line 41
  4. def OAI.LowSpaceSubsetSum.WordSeedMeasured.nestedPrepared line 48
  5. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.extra_width line 54
  6. def OAI.LowSpaceSubsetSum.WordSeedMeasured.extraAtWidth line 61
  7. def OAI.LowSpaceSubsetSum.WordSeedMeasured.extraFromPrepared line 71
  8. def OAI.LowSpaceSubsetSum.WordSeedMeasured.extraPrepared line 77