OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedRealization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Fair-word programs returning successful bounded sampler seeds

Failure returns no seed. Success retains the actual candidate tuples, so the prepared algorithm can consume the bounded sampler seed type. Only the law of the observed bounded output is asserted; unused backup coordinates need not have their ideal distribution.

  1. def OAI.LowSpaceSubsetSum.WordSeedRealization.SuccessfulSeed line 21
  2. def OAI.LowSpaceSubsetSum.WordSeedRealization.observe line 24
  3. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.successful_agrees line 27
  4. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.observe_some line 35
  5. structure OAI.LowSpaceSubsetSum.WordSeedRealization.Realization line 38
  6. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.bind_assoc line 44
  7. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.map_bind line 52
  8. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.bind_map line 58
  9. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.map_map line 65
  10. def OAI.LowSpaceSubsetSum.WordSeedRealization.toRealization line 69
  11. def OAI.LowSpaceSubsetSum.WordSeedRealization.pure line 78
  12. def OAI.LowSpaceSubsetSum.WordSeedRealization.mapSeed line 83
  13. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.observe_map line 92
  14. def OAI.LowSpaceSubsetSum.WordSeedRealization.map line 96
  15. def OAI.LowSpaceSubsetSum.WordSeedRealization.pairSeed line 116
  16. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.observe_pair line 125
  17. def OAI.LowSpaceSubsetSum.WordSeedRealization.continuation line 137
  18. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.continuation_observed line 143
  19. def OAI.LowSpaceSubsetSum.WordSeedRealization.bind line 157