OAI/Combinatorics/EditApproximation/Binary/BinaryBandGuardWork.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Exact finite band predicates evaluated on stored Boolean fractions. The cut tests use the actual finite prefix minimum; the other tests are Boolean comparisons of the actual interval endpoints.

  1. theorem OAI.EditApproximation.naturalEqualWithWork_value line 19
  2. theorem OAI.EditApproximation.naturalEqualWithWork_cost line 23
  3. theorem OAI.EditApproximation.zeroConnectionWithWork_value line 31
  4. theorem OAI.EditApproximation.zeroConnectionWithWork_cost line 51
  5. theorem OAI.EditApproximation.translatedEndpointWithWork_value line 73

    Source documentation

    Construct a translated endpoint by the actual binary subtract/add routines.

    @[simp] theorem translatedEndpointWithWork_value (reference root endpoint : ℕ) (h : root ≤ endpoint) :
    (translatedEndpointWithWork reference root endpoint).1 = reference + (endpoint - root) := by
…

    Mentions: OAI.EditApproximation.translatedEndpointWithWork

  6. theorem OAI.EditApproximation.translatedEndpointWithWork_cost line 78
  7. theorem OAI.EditApproximation.BinaryFraction.nat_dist_cast line 93
  8. theorem OAI.EditApproximation.BinaryFraction.naturalDistanceLeWithWork_value line 101
  9. def OAI.EditApproximation.BinaryFraction.naturalDistanceBitBudget line 107
  10. theorem OAI.EditApproximation.BinaryFraction.naturalDistanceLeWithWork_cost line 110
  11. def OAI.EditApproximation.BinaryFraction.cutGuardWithWork line 125
  12. theorem OAI.EditApproximation.BinaryFraction.cutGuardWithWork_value line 137
  13. def OAI.EditApproximation.BinaryFraction.cutGuardWordBudget line 157
  14. def OAI.EditApproximation.BinaryFraction.cutGuardBitBudget line 160
  15. theorem OAI.EditApproximation.BinaryFraction.cutGuardWithWork_cost line 165
  16. def OAI.EditApproximation.BinaryFraction.bandPredicateWithWork line 211
  17. theorem OAI.EditApproximation.BinaryFraction.bandPredicateWithWork_value line 228
  18. def OAI.EditApproximation.BinaryFraction.anchorGuardBitBudget line 244
  19. def OAI.EditApproximation.BinaryFraction.bandPredicateBitBudget line 247
  20. theorem OAI.EditApproximation.BinaryFraction.bandPredicateWithWork_cost line 251