OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSamplingBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete word draw buffer fits below the branch workspace

  1. theorem OAI.LowSpaceSubsetSum.WordSamplingBounds.family_width line 14
  2. theorem OAI.LowSpaceSubsetSum.WordSamplingBounds.family_codes line 19
  3. theorem OAI.LowSpaceSubsetSum.WordSamplingBounds.history_normalize line 25
  4. theorem OAI.LowSpaceSubsetSum.WordSamplingBounds.history_reads line 31
  5. theorem OAI.LowSpaceSubsetSum.WordSamplingBounds.word_width line 60
  6. def OAI.LowSpaceSubsetSum.WordSamplingBounds.representation line 64
  7. theorem OAI.LowSpaceSubsetSum.WordSamplingBounds.representation_probability line 69