OAI/Combinatorics/LowSpaceSubsetSum/Counting/MatchPotential.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Potential matching occurrences in sorted streams

This count uses list occurrences, so repeated values and equal records are counted separately. Removing a completed equal-key group subtracts its full Cartesian product; this is the potential used to charge stopped replays.

  1. def OAI.LowSpaceSubsetSum.MatchPotential.count line 18
  2. theorem OAI.LowSpaceSubsetSum.MatchPotential.positive_iff line 22
  3. theorem OAI.LowSpaceSubsetSum.MatchPotential.append_left line 40
  4. theorem OAI.LowSpaceSubsetSum.MatchPotential.append_right line 46
  5. theorem OAI.LowSpaceSubsetSum.MatchPotential.eq_zero line 52
  6. theorem OAI.LowSpaceSubsetSum.MatchPotential.eq_product line 64
  7. theorem OAI.LowSpaceSubsetSum.MatchPotential.split_groups line 78
  8. theorem OAI.LowSpaceSubsetSum.MatchPotential.sorted_dropWhile_avoids line 95
  9. theorem OAI.LowSpaceSubsetSum.MatchPotential.remaining_eq_dropWhile line 114
  10. theorem OAI.LowSpaceSubsetSum.MatchPotential.remaining_sublist line 119
  11. theorem OAI.LowSpaceSubsetSum.MatchPotential.remaining_avoids line 124
  12. theorem OAI.LowSpaceSubsetSum.MatchPotential.lower_bound_head line 131
  13. theorem OAI.LowSpaceSubsetSum.MatchPotential.skip_left line 139
  14. theorem OAI.LowSpaceSubsetSum.MatchPotential.skip_right line 148