OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionDictionary.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The compressed trial's actual lists and bounded solution dictionary

Raw lists enumerate indexed subsets and retain repeated weights. The seven block lists sort these weights and remove duplicates. Their four generated pair-sum lists are proof views of the streams; their full products need not be stored by the implementation.

  1. theorem OAI.LowSpaceSubsetSum.compressionRightRaw_lower line 19
  2. theorem OAI.LowSpaceSubsetSum.compressionBlock_rightRaw_disjoint line 23
  3. theorem OAI.LowSpaceSubsetSum.compressionLeftRaw_rightRaw_disjoint line 35
  4. theorem OAI.LowSpaceSubsetSum.compressionRightRaw_disjoint line 45
  5. def OAI.LowSpaceSubsetSum.rawWeightList line 52
  6. theorem OAI.LowSpaceSubsetSum.mem_rawWeightList line 55
  7. theorem OAI.LowSpaceSubsetSum.rawWeightList_length line 76
  8. def OAI.LowSpaceSubsetSum.compactWeightList line 80
  9. theorem OAI.LowSpaceSubsetSum.mem_compactWeightList line 83
  10. theorem OAI.LowSpaceSubsetSum.compactWeightList_toFinset line 89
  11. theorem OAI.LowSpaceSubsetSum.compactWeightList_length line 94
  12. def OAI.LowSpaceSubsetSum.pairSumList line 100
  13. theorem OAI.LowSpaceSubsetSum.mem_pairSumList line 102
  14. theorem OAI.LowSpaceSubsetSum.pairSumList_length line 111
  15. theorem OAI.LowSpaceSubsetSum.distinctSums_union_mem_iff line 116
  16. theorem OAI.LowSpaceSubsetSum.CompressionSetup.blocks_disjoint line 134
  17. theorem OAI.LowSpaceSubsetSum.CompressionSetup.block_leftRaw_disjoint line 138
  18. theorem OAI.LowSpaceSubsetSum.CompressionSetup.block_rightRaw_disjoint line 142
  19. theorem OAI.LowSpaceSubsetSum.CompressionSetup.rightRaws_disjoint line 146
  20. theorem OAI.LowSpaceSubsetSum.CompressionSetup.left_groups_disjoint line 150
  21. theorem OAI.LowSpaceSubsetSum.CompressionSetup.right_groups_disjoint line 160
  22. theorem OAI.LowSpaceSubsetSum.CompressionSetup.groupDomains_disjoint line 176
  23. def OAI.LowSpaceSubsetSum.CompressionSetup.storedFirst line 198
  24. def OAI.LowSpaceSubsetSum.CompressionSetup.storedSecond line 202
  25. def OAI.LowSpaceSubsetSum.CompressionSetup.groupList line 207
  26. theorem OAI.LowSpaceSubsetSum.CompressionSetup.mem_groupList line 210
  27. theorem OAI.LowSpaceSubsetSum.CompressionSetup.groupList_toFinset line 242