OAI/Combinatorics/LowSpaceSubsetSum/Streams/Tournament.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Cached tournament for merging row fronts

Each leaf holds at most one current occurrence of a row. Internal nodes cache the smaller child winner. Reading the winner is constant time; replacing one leaf recomputes just its root path. The candidate list below is an analysis view and is never stored in the tournament.

  1. def OAI.LowSpaceSubsetSum.Tournament.pick line 24
  2. theorem OAI.LowSpaceSubsetSum.Tournament.pick_member line 29
  3. theorem OAI.LowSpaceSubsetSum.Tournament.pick_le_left line 41
  4. theorem OAI.LowSpaceSubsetSum.Tournament.pick_le_right line 50
  5. def OAI.LowSpaceSubsetSum.Tournament.Best line 59
  6. theorem OAI.LowSpaceSubsetSum.Tournament.best_append line 62
  7. inductive OAI.LowSpaceSubsetSum.Tournament.Tree line 81
  8. def OAI.LowSpaceSubsetSum.Tournament.winner line 85
  9. def OAI.LowSpaceSubsetSum.Tournament.candidates line 89
  10. def OAI.LowSpaceSubsetSum.Tournament.Valid line 93
  11. def OAI.LowSpaceSubsetSum.Tournament.node line 97
  12. theorem OAI.LowSpaceSubsetSum.Tournament.winner_best line 100
  13. theorem OAI.LowSpaceSubsetSum.Tournament.winner_none_iff line 110
  14. def OAI.LowSpaceSubsetSum.Tournament.lookup line 124
  15. def OAI.LowSpaceSubsetSum.Tournament.replace line 129
  16. theorem OAI.LowSpaceSubsetSum.Tournament.replace_valid line 135
  17. theorem OAI.LowSpaceSubsetSum.Tournament.lookup_replace_same line 147
  18. theorem OAI.LowSpaceSubsetSum.Tournament.lookup_replace line 155
  19. def OAI.LowSpaceSubsetSum.Tournament.build line 175
  20. theorem OAI.LowSpaceSubsetSum.Tournament.build_valid line 181
  21. theorem OAI.LowSpaceSubsetSum.Tournament.lookup_build line 187
  22. theorem OAI.LowSpaceSubsetSum.Tournament.mem_candidates_iff line 207
  23. theorem OAI.LowSpaceSubsetSum.Tournament.winner_le_lookup line 227
  24. def OAI.LowSpaceSubsetSum.Tournament.nodes line 232
  25. theorem OAI.LowSpaceSubsetSum.Tournament.nodes_exact line 236
  26. theorem OAI.LowSpaceSubsetSum.Tournament.padded_nodes_le line 244
  27. theorem OAI.LowSpaceSubsetSum.Tournament.depth_le_index_bits line 260
  28. def OAI.LowSpaceSubsetSum.Tournament.replaceComparisons line 264

    Source documentation

    Number of cached comparisons made by a leaf replacement.

    def replaceComparisons : {d : ℕ} → Tree α d → (Fin d → Bool) → ℕ
  | 0, .leaf _, _ => 0
  | _d + 1, .node _ l r, path =>
    1 + if path 0 then replaceComparisons r (fun i => path i.succ)
      else replaceComparisons l (fun i => path i.succ)

    Mentions: OAI.LowSpaceSubsetSum.Tournament.Tree, OAI.LowSpaceSubsetSum.Tournament.node

  29. theorem OAI.LowSpaceSubsetSum.Tournament.replaceComparisons_eq line 270