OAI/Combinatorics/EditApproximation/Coarse/CoarseThresholdArithmetic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Boolean threshold arithmetic on the fixed denominator of one coarse execution. Quotients use actual long division when compressed to that grid.

  1. theorem OAI.EditApproximation.BinaryFraction.coarseDivideWithWork_value line 16
  2. theorem OAI.EditApproximation.BinaryFraction.coarseDivideWithWork_den line 24
  3. theorem OAI.EditApproximation.BinaryFraction.coarseDivideWithWork_cost line 28
  4. theorem OAI.EditApproximation.BinaryFraction.coarseDivideWithWork_width line 39
  5. theorem OAI.EditApproximation.BinaryFraction.coarseContributionWithWork_value line 50

    Source documentation

    The exact branch and maximum used for each transformed child cell.

     theorem coarseContributionWithWork_value (threshold scale a : BinaryFraction) :
    (coarseContributionWithWork threshold scale a).1.value =
      coarseThresholdContribution threshold.value scale.value a.value := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.coarseContributionWithWork, OAI.EditApproximation.BinaryFraction.value, OAI.EditApproximation.coarseThresholdContribution

  6. theorem OAI.EditApproximation.BinaryFraction.coarseContributionWithWork_den line 61
  7. theorem OAI.EditApproximation.BinaryFraction.coarseContributionWithWork_cost line 74