OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorTraversal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Depth-first separator interval traversal

Only the received arrays, their filtered children and a scalar result are retained. A branch whose filtered arrays are empty ends immediately. The binary interval queries refer to the precomputed incidence arrays. The terminal callback is the next block, or the final exact-weight search.

  1. structure OAI.LowSpaceSubsetSum.SeparatorTraversal.Result line 20
  2. def OAI.LowSpaceSubsetSum.SeparatorTraversal.keep line 26
  3. def OAI.LowSpaceSubsetSum.SeparatorTraversal.finish line 29
  4. def OAI.LowSpaceSubsetSum.SeparatorTraversal.run line 35

    Source documentation

    The ledger completes both children, so acceptance can only save work.

    def run (inc₁ : α → Array ℕ) (inc₂ : β → Array ℕ)
    (leaf : ℕ → List α → List β → Result) : ℕ → ℕ → ℕ → List α → List β → Result
  | 0, lo, hi, xs, ys =>
    let left := keep inc₁ lo hi xs
…

    Mentions: OAI.LowSpaceSubsetSum.SeparatorTraversal.Result, OAI.LowSpaceSubsetSum.SeparatorTraversal.keep

  5. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.keep_mem line 57
  6. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.keep_length line 61
  7. def OAI.LowSpaceSubsetSum.SeparatorTraversal.Witness line 64
  8. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.witness_empty line 69
  9. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.witness_singleton line 86
  10. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.witness_split line 106
  11. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.correct line 129
  12. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.peak_le line 169

    Source documentation

    Retaining parent buffers through both children costs only depth times input length, plus the terminal callback's workspace.

    theorem peak_le (inc₁ : α → Array ℕ) (inc₂ : β → Array ℕ)
    (leaf : ℕ → List α → List β → Result) (L : ℕ)
    (hleaf : ∀ j xs ys, (leaf j xs ys).peak ≤ L)
    (k lo hi : ℕ) (xs : List α) (ys : List β) :
    (run inc₁ inc₂ leaf k lo hi xs ys).peak ≤
      2 * (k + 1) * (xs.length + ys.length) + L := by
…

    Mentions: OAI.LowSpaceSubsetSum.SeparatorTraversal.Result, OAI.LowSpaceSubsetSum.SeparatorTraversal.run

  13. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.peak_le_capacity line 200

    Source documentation

    Retaining parent buffers through both children costs only depth times input length, plus the terminal callback's workspace.

    theorem peak_le_capacity (inc₁ : α → Array ℕ) (inc₂ : β → Array ℕ)
    (leaf : ℕ → List α → List β → Result) (C L : ℕ)
    (hleaf : ∀ j xs ys, xs.length + ys.length ≤ C → (leaf j xs ys).peak ≤ L)
    (k lo hi : ℕ) (xs : List α) (ys : List β) (hsize : xs.length + ys.length ≤ C) :
    (run inc₁ inc₂ leaf k lo hi xs ys).peak ≤
      2 * (k + 1) * (xs.length + ys.length) + L := by
…

    Mentions: OAI.LowSpaceSubsetSum.SeparatorTraversal.Result, OAI.LowSpaceSubsetSum.SeparatorTraversal.run