OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorTraversalCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Occurrence charges for the separator traversal

Every occurrence has its own incidence multiplicity. The charge includes one scan even when that multiplicity is zero; terminal charges are multiplied by the number of compatible indices, with no Cartesian pair enumeration.

  1. def OAI.LowSpaceSubsetSum.SeparatorTraversal.mass line 19
  2. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.mass_split line 22
  3. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.mass_keep line 32
  4. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.kept_charge_le_mass line 46
  5. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.keep_length_le_mass line 62
  6. theorem OAI.LowSpaceSubsetSum.SeparatorTraversal.scans_le line 70

    Source documentation

    Scans charged to each original occurrence, plus the supplied per-occurrence terminal work. At depth zero a zero-incidence record still pays its root scan.

    theorem scans_le (inc₁ : α → Array ℕ) (inc₂ : β → Array ℕ)
    (leaf : ℕ → List α → List β → Result)
    (hs₁ : ∀ x, Monotone (fun i : Fin (inc₁ x).size => (inc₁ x)[i.val]))
    (hs₂ : ∀ y, Monotone (fun i : Fin (inc₂ y).size => (inc₂ y)[i.val]))
    (charge₁ : α → ℕ) (charge₂ : β → ℕ)
    (hleaf : ∀ j xs ys, (leaf j xs ys).scans ≤
      (xs.map charge₁).sum + (ys.map charge₂).sum)
    (k lo hi : ℕ) (xs : List α) (ys : List β) :
    (run inc₁ inc₂ leaf k lo hi xs ys).scans ≤
      xs.length + ys.length +
      2 * k * (mass inc₁ lo hi xs (fun _ => 1) + mass inc₂ lo hi ys (fun _ => 1)) +
      mass inc₁ lo hi xs charge₁ + mass inc₂ lo hi ys charge₂ := by
…

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