OAI/Combinatorics/EditApproximation/Geometry/LocalWorkEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Multiplying the actual charged dependency-tree work by the concrete local arithmetic counter preserves the almost-linear exponent.

  1. theorem OAI.EditApproximation.computed_widthWork_subexponential line 14
  2. theorem OAI.EditApproximation.computed_local_arithmetic_widthWork_near_linear line 37