OAI/Combinatorics/LowSpaceSubsetSum/Storage/LeafEnumeration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Executable indexed raw-leaf enumeration

  1. def OAI.LowSpaceSubsetSum.subsetList line 13

    Source documentation

    Each indexed subset is generated in the fixed input-index order.

    def subsetList (V : Finset (Fin n)) : List (Finset (Fin n)) :=
…
  2. def OAI.LowSpaceSubsetSum.fixedSubsetList line 17

    Source documentation

    Fixed-size selections use the corresponding finite sublist generator.

    def fixedSubsetList (V : Finset (Fin n)) (k : ℕ) : List (Finset (Fin n)) :=
…
  3. theorem OAI.LowSpaceSubsetSum.subsetList_mem line 20
  4. theorem OAI.LowSpaceSubsetSum.fixedSubsetList_mem line 35
  5. theorem OAI.LowSpaceSubsetSum.subsetList_length line 55
  6. theorem OAI.LowSpaceSubsetSum.fixedSubsetList_length line 58
  7. def OAI.LowSpaceSubsetSum.RepresentationLeaf.enumerate line 65

    Source documentation

    Raw leaves retain the three subset choices, including repeated weights.

    def enumerate (L : RepresentationLeaf (Fin n)) : List (Occurrence (Fin n)) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationLeaf.Occurrence

  8. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.enumerate_mem line 69
  9. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.enumerate_length line 75
  10. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.enumerate_toFinset line 81
  11. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.enumerate_nodup line 85