OAI/Combinatorics/EditApproximation/Binary/BinaryFixedDenominator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact cache-value compression to a prescribed denominator. It performs one Boolean multiplication and one Boolean long division, followed only by leading-zero removal. No rational gcd or reduced-rational conversion is used.

  1. theorem OAI.EditApproximation.BinaryFraction.raw_den_dvd_scaled_num line 15
  2. theorem OAI.EditApproximation.BinaryFraction.fixedDenominatorWithWork_value line 35
  3. theorem OAI.EditApproximation.BinaryFraction.fixedDenominatorWithWork_den line 71
  4. theorem OAI.EditApproximation.BinaryFraction.fixedDenominatorWithWork_width line 79
  5. theorem OAI.EditApproximation.BinaryFraction.fixedDenominatorWithWork_cost line 101