OAI/Combinatorics/EditApproximation/Binary/BinaryPrefixWork.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal stored-fraction evaluation of the finite prefix predictor. Every prefix minimum scans the finite action array and uses exact Boolean comparisons. No rational operation is assigned unit cost.

  1. def OAI.EditApproximation.BinaryFraction.prefixWithWork line 14
  2. theorem OAI.EditApproximation.BinaryFraction.prefixWithWork_value line 26
  3. def OAI.EditApproximation.BinaryFraction.prefixConnectionWord line 38
  4. def OAI.EditApproximation.BinaryFraction.prefixWordBudget line 40
  5. def OAI.EditApproximation.BinaryFraction.prefixBitBudget line 43
  6. theorem OAI.EditApproximation.BinaryFraction.prefix_parts line 49
  7. theorem OAI.EditApproximation.BinaryFraction.prefixWithWork_width line 95
  8. theorem OAI.EditApproximation.BinaryFraction.prefixWithWork_cost line 107
  9. def OAI.EditApproximation.BinaryFraction.prefixMinimumWithWork line 126
  10. theorem OAI.EditApproximation.BinaryFraction.prefixMinimumWithWork_value line 135
  11. def OAI.EditApproximation.BinaryFraction.prefixMinimumBitBudget line 143
  12. theorem OAI.EditApproximation.BinaryFraction.prefixMinimumWithWork_bounds line 147