OAI/Combinatorics/EditApproximation/Binary/BinaryWideGridWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial per-child bit work before the explicitly counted Cartesian product. All interval endpoints and arities are bounded by their input word sizes; no good-seed premise occurs in these bounds.

  1. theorem OAI.EditApproximation.balancedCutWithWork_cost line 12
  2. theorem OAI.EditApproximation.sourceChildWithWork_cost line 34