OAI/Combinatorics/LowSpaceSubsetSum/Storage/FiniteSetCells.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded scans of an already stored finite set

The membership scan is tail recursive and visits the stored list once. Its value, full-scan work, and constant workspace are invariant under list permutation, so the executable descends through the multiset quotient without extracting a representative by choice.

  1. def OAI.LowSpaceSubsetSum.FiniteSetCells.scan line 18
  2. theorem OAI.LowSpaceSubsetSum.FiniteSetCells.scan_formula line 22
  3. def OAI.LowSpaceSubsetSum.FiniteSetCells.multisetMember line 33
  4. theorem OAI.LowSpaceSubsetSum.FiniteSetCells.multisetMember_formula line 38
  5. def OAI.LowSpaceSubsetSum.FiniteSetCells.member line 45
  6. theorem OAI.LowSpaceSubsetSum.FiniteSetCells.member_formula line 47
  7. def OAI.LowSpaceSubsetSum.FiniteSetCells.domain line 51
  8. theorem OAI.LowSpaceSubsetSum.FiniteSetCells.domain_value line 55
  9. theorem OAI.LowSpaceSubsetSum.FiniteSetCells.domain_cells line 60
  10. theorem OAI.LowSpaceSubsetSum.FiniteSetCells.domain_filter_work line 69

    Source documentation

    The work of the full scans fits the domain reserve.

    theorem domain_filter_work (V : Finset (Fin n)) :
    (MeasuredFilterCells.run (member V) (List.finRange n)).1.2 ≤ 2*(n+1)^2 := by
…

    Mentions: OAI.LowSpaceSubsetSum.MeasuredFilterCells.run, OAI.LowSpaceSubsetSum.FiniteSetCells.member