OAI/Combinatorics/LowSpaceSubsetSum/Compression/BudgetedCompressionJoin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete compression joins with an execution watchdog

The input arrays are shared, snapshots copy only the right tournament, and callbacks execute the bounded dictionary operations. The charge is independent of the queried values and of the success event.

  1. def OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.reference line 23
  2. def OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.run line 33
  3. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.reference_value line 45
  4. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.run_value line 57
  5. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.operation_charge line 66
  6. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.run_work line 74
  7. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.query_charge line 102
  8. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.account line 112
  9. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.run_complete line 145
  10. theorem OAI.LowSpaceSubsetSum.BudgetedCompressionJoin.run_remaining line 166