OAI/Combinatorics/LowSpaceSubsetSum/Streams/MergeOrdering.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Sortedness of complete and stopped row merges

Only each row's individual order is required. The tournament minimum is no larger than every remaining occurrence; replacing its front by its successor preserves this invariant. Every finite trace is therefore sorted, including traces stopped by the operation cap.

  1. def OAI.LowSpaceSubsetSum.RowMerge.RowsSorted line 21
  2. theorem OAI.LowSpaceSubsetSum.RowMerge.replacement_remaining_subset line 25
  3. theorem OAI.LowSpaceSubsetSum.RowMerge.replacement_rowsSorted line 43
  4. theorem OAI.LowSpaceSubsetSum.RowMerge.winner_le_remaining line 63
  5. theorem OAI.LowSpaceSubsetSum.RowMerge.trace_lower_bound line 78
  6. theorem OAI.LowSpaceSubsetSum.RowMerge.trace_sorted line 105