OAI/Combinatorics/EditApproximation/Binary/BinaryAffineGuard.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Boolean tests for the affine errors in band membership. The literal product, both subtractions and final comparison have charged bit work.

  1. theorem OAI.EditApproximation.BinaryFraction.canonicalMulWithWork_width line 13
  2. theorem OAI.EditApproximation.BinaryFraction.affineErrorWithWork_value line 25
  3. def OAI.EditApproximation.BinaryFraction.affineGuardBitBudget line 31
  4. theorem OAI.EditApproximation.BinaryFraction.affineErrorWithWork_cost line 36
  5. theorem OAI.EditApproximation.BinaryFraction.bandToleranceWithWork_value line 59

    Source documentation

    Threshold used in every internal-cut predicate.

    @[simp] theorem bandToleranceWithWork_value (tau theta : BinaryFraction) (b M : ℕ) :
    (bandToleranceWithWork tau theta b M).1.value = tau.value * theta.value * b / M := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.bandToleranceWithWork, OAI.EditApproximation.BinaryFraction.value

  6. theorem OAI.EditApproximation.BinaryFraction.divWithWork_width_uniform line 63
  7. def OAI.EditApproximation.BinaryFraction.bandToleranceBitBudget line 73
  8. theorem OAI.EditApproximation.BinaryFraction.bandToleranceWithWork_bounds line 77