OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionSoundness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One-sided soundness of compression on every input and family outcome

  1. theorem OAI.LowSpaceSubsetSum.CompressionData.actualLeftDictionary_provenance line 12
  2. theorem OAI.LowSpaceSubsetSum.CompressionData.rightPair_mem line 36
  3. theorem OAI.LowSpaceSubsetSum.CompressionData.actualRightHit_provenance line 44
  4. theorem OAI.LowSpaceSubsetSum.CompressionData.subset_weight_bound line 65
  5. theorem OAI.LowSpaceSubsetSum.CompressionData.distinct_weight_bound line 71
  6. theorem OAI.LowSpaceSubsetSum.CompressionData.residuePass_sound line 76
  7. theorem OAI.LowSpaceSubsetSum.CompressionData.compressionTrial_sound line 104
  8. def OAI.LowSpaceSubsetSum.CompressionData.trialLaw line 112
  9. theorem OAI.LowSpaceSubsetSum.CompressionData.compressionTrial_probability line 115