OAI/Combinatorics/EditApproximation/Binary/BinaryCoordinateActionWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The cost of coordinate construction and every endpoint equality is added to the complete optimizer cost, with no unit-cost rational or uncharged generic equality operation.

  1. theorem OAI.EditApproximation.BinaryFraction.vectorMap_cost_le_add line 12
  2. theorem OAI.EditApproximation.BinaryFraction.countedBandVerticesWithWork_cost line 23
  3. theorem OAI.EditApproximation.BinaryFraction.countedPreparedActionWithWork_cost line 58
  4. theorem OAI.EditApproximation.BinaryFraction.countedBandActionWithWork_cost line 78
  5. theorem OAI.EditApproximation.BinaryFraction.countedSampledOnlineWithWork_cost line 93