OAI/Combinatorics/EditApproximation/Geometry/DependencyWeightedWork.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Width-sensitive work summed over an actual finite dependency expansion. The bound uses its per-layer counts, including earlier edges that descend.

  1. def OAI.EditApproximation.DependencyExpansion.widthWork line 16
  2. theorem OAI.EditApproximation.DependencyExpansion.widthWork_le line 19
  3. theorem OAI.EditApproximation.DependencyExpansion.computed_widthWork_subpolynomial line 60