OAI/Combinatorics/EditApproximation/Binary/BinaryMaximizerWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Counted stored-score maximization for Boolean fraction coordinates.

  1. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork_score_width line 12
  2. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork_cost line 25
  3. def OAI.EditApproximation.BinaryFraction.maximizerWordBudget line 47
  4. def OAI.EditApproximation.BinaryFraction.maximizerBitBudget line 49
  5. theorem OAI.EditApproximation.BinaryFraction.maximizerWithWork_cost line 53