OAI/Combinatorics/LowSpaceSubsetSum/Streams/SumReader.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Counting a mixer through a tournament of ordinary sum rows

Only the two half-mixer arrays and a tournament of constant-size cursors are stored. The output lists in the proofs are views, not runtime fields. Sorting and counting use integer sums and require no modulus or real oracle.

  1. structure OAI.LowSpaceSubsetSum.SumReader.Row line 18
  2. def OAI.LowSpaceSubsetSum.SumReader.read line 22
  3. def OAI.LowSpaceSubsetSum.SumReader.view line 27
  4. theorem OAI.LowSpaceSubsetSum.SumReader.reader line 30
  5. def OAI.LowSpaceSubsetSum.SumReader.key line 40
  6. def OAI.LowSpaceSubsetSum.SumReader.rows line 42
  7. theorem OAI.LowSpaceSubsetSum.SumReader.row_sorted line 44
  8. abbrev OAI.LowSpaceSubsetSum.SumReader.State line 50
  9. def OAI.LowSpaceSubsetSum.SumReader.start line 53
  10. def OAI.LowSpaceSubsetSum.SumReader.next line 59
  11. def OAI.LowSpaceSubsetSum.SumReader.output line 63
  12. theorem OAI.LowSpaceSubsetSum.SumReader.next_law line 66
  13. theorem OAI.LowSpaceSubsetSum.SumReader.output_sorted line 69
  14. theorem OAI.LowSpaceSubsetSum.SumReader.start_bag line 74
  15. theorem OAI.LowSpaceSubsetSum.SumReader.output_mem line 88
  16. theorem OAI.LowSpaceSubsetSum.SumReader.output_length line 102
  17. def OAI.LowSpaceSubsetSum.SumReader.count line 108
  18. theorem OAI.LowSpaceSubsetSum.SumReader.count_value line 111
  19. theorem OAI.LowSpaceSubsetSum.SumReader.count_queries line 116
  20. def OAI.LowSpaceSubsetSum.SumReader.footprint line 120

    Source documentation

    Every cursor and cached front occupies a constant number of flat cells.

    def footprint (xs ys : Array ℤ) (s : State xs ys) : ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.SumReader.State

  21. theorem OAI.LowSpaceSubsetSum.SumReader.footprint_bound line 123