OAI/Combinatorics/LowSpaceSubsetSum/Streams/PaddedRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Binary indexing and empty padding for the row tournament

Binary paths index a power-of-two set of leaves. Array indices occupy the initial segment and all other leaves are empty. The reindexing proof counts exact occurrences; its finite sums and lists are analysis views only.

  1. def OAI.LowSpaceSubsetSum.PaddedRows.index line 19
  2. def OAI.LowSpaceSubsetSum.PaddedRows.next line 22
  3. def OAI.LowSpaceSubsetSum.PaddedRows.view line 26
  4. theorem OAI.LowSpaceSubsetSum.PaddedRows.reader line 30
  5. def OAI.LowSpaceSubsetSum.PaddedRows.rows line 41
  6. theorem OAI.LowSpaceSubsetSum.PaddedRows.rows_sorted line 44
  7. theorem OAI.LowSpaceSubsetSum.PaddedRows.sum_padding line 55
  8. theorem OAI.LowSpaceSubsetSum.PaddedRows.sum_rows line 75
  9. theorem OAI.LowSpaceSubsetSum.PaddedRows.row_bag line 87