OAI/Combinatorics/EditApproximation/Binary/BinaryRepresentativeWork.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the executed representative scores and velocity. They use only the widths of actual stored inputs, and apply on every seed.

  1. def OAI.EditApproximation.BinaryFraction.endpointDistanceWordBudget line 14
  2. def OAI.EditApproximation.BinaryFraction.endpointDistanceBitBudget line 16
  3. theorem OAI.EditApproximation.BinaryFraction.endpointDistanceWithWork_bounds line 19
  4. def OAI.EditApproximation.BinaryFraction.endpointScoreWordBudget line 46
  5. def OAI.EditApproximation.BinaryFraction.endpointScoreBitBudget line 49
  6. theorem OAI.EditApproximation.BinaryFraction.endpointScoreWithWork_bounds line 53
  7. def OAI.EditApproximation.BinaryFraction.wideMinimumBitBudget line 91
  8. theorem OAI.EditApproximation.BinaryFraction.wideMinimumWithWork_bounds line 95
  9. def OAI.EditApproximation.BinaryFraction.stateGapWordBudget line 129
  10. def OAI.EditApproximation.BinaryFraction.stateGapBitBudget line 131
  11. theorem OAI.EditApproximation.BinaryFraction.stateGapWithWork_bounds line 134