OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionStoppedAcceptance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded-sampler acceptance of the executed compression trial

The accepted event requires a completed shared-budget execution, from array generation to the final residue. Watchdog failure returns false.

  1. def OAI.LowSpaceSubsetSum.CompressionData.stoppedCompressionTrial line 17
  2. theorem OAI.LowSpaceSubsetSum.CompressionData.stoppedCompressionTrial_accepts line 22
  3. theorem OAI.LowSpaceSubsetSum.CompressionData.stoppedCompressionTrial_sound line 28
  4. theorem OAI.LowSpaceSubsetSum.CompressionData.bounded_stoppedCompression_probability line 39