OAI/Combinatorics/LowSpaceSubsetSum/Search/StoppedSamplerLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The law of a dependent sampler that stops on exhaustion

Only an actual successful first value selects the next distribution. The ideal completion of a failed first call disappears from this formula.

  1. def OAI.LowSpaceSubsetSum.StoppedSamplerLaw.nextProbability line 19
  2. theorem OAI.LowSpaceSubsetSum.StoppedSamplerLaw.bind_probability line 24