OAI/Combinatorics/LowSpaceSubsetSum/Word/WordRealization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact fair-word refinements of the stopped sampler constructors

  1. structure OAI.LowSpaceSubsetSum.WordRealization.Realization line 14
  2. def OAI.LowSpaceSubsetSum.WordRealization.pure line 21
  3. def OAI.LowSpaceSubsetSum.WordRealization.map line 32
  4. def OAI.LowSpaceSubsetSum.WordRealization.continuation line 45
  5. theorem OAI.LowSpaceSubsetSum.WordRealization.continuation_probability line 52
  6. def OAI.LowSpaceSubsetSum.WordRealization.bind line 62
  7. def OAI.LowSpaceSubsetSum.WordRealization.rejection line 85