OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedSubsets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Output-sensitive fixed-cardinality subset generation

Infeasible recursive branches are pruned before they recurse. The work counter charges the feasibility scan, recursive calls, append and map; this avoids charging all subsets of a block when only one cardinality is needed.

  1. def OAI.LowSpaceSubsetSum.CountedSubsets.all line 16
  2. theorem OAI.LowSpaceSubsetSum.CountedSubsets.all_value line 22
  3. theorem OAI.LowSpaceSubsetSum.CountedSubsets.all_length line 27
  4. theorem OAI.LowSpaceSubsetSum.CountedSubsets.all_work line 30
  5. def OAI.LowSpaceSubsetSum.CountedSubsets.select line 38
  6. theorem OAI.LowSpaceSubsetSum.CountedSubsets.select_value line 51
  7. theorem OAI.LowSpaceSubsetSum.CountedSubsets.select_length line 67
  8. theorem OAI.LowSpaceSubsetSum.CountedSubsets.select_infeasible line 71
  9. theorem OAI.LowSpaceSubsetSum.CountedSubsets.select_work line 82

    Source documentation

    The count is quadratic in the domain length and linear in the exact number of selected subsets, including the boundary cases k=0 and k=n.

    theorem select_work (k : ℕ) (xs : List α) (hk : k ≤ xs.length) :
    (select k xs).2 ≤ 4 * (xs.length + 1) ^ 2 * xs.length.choose k := by
…

    Mentions: OAI.LowSpaceSubsetSum.CountedSubsets.select