OAI/Combinatorics/EditApproximation/Binary/UnreducedNumerics.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The numerical primitives executed on unreduced fractions. Their exact values agree with the rational routines; their stored denominators have polynomial bit length without cancellation or Euclidean normalization.

  1. def OAI.EditApproximation.UnreducedRational.one line 17
  2. def OAI.EditApproximation.UnreducedRational.sub line 21
  3. def OAI.EditApproximation.UnreducedRational.pow line 23
  4. theorem OAI.EditApproximation.UnreducedRational.value_one line 27
  5. theorem OAI.EditApproximation.UnreducedRational.value_nat line 28
  6. theorem OAI.EditApproximation.UnreducedRational.value_sub line 29
  7. theorem OAI.EditApproximation.UnreducedRational.value_pow line 32
  8. theorem OAI.EditApproximation.UnreducedRational.pow_den line 37
  9. theorem OAI.EditApproximation.UnreducedRational.pow_den_bits line 42
  10. theorem OAI.EditApproximation.UnreducedRational.nat_inv_den line 47
  11. def OAI.EditApproximation.UnreducedRational.logarithmPartial line 50
  12. def OAI.EditApproximation.UnreducedRational.logarithm line 54
  13. theorem OAI.EditApproximation.UnreducedRational.logarithmPartial_value line 57
  14. theorem OAI.EditApproximation.UnreducedRational.logarithm_value line 64
  15. theorem OAI.EditApproximation.UnreducedRational.logarithmPartial_den_bits line 68
  16. theorem OAI.EditApproximation.UnreducedRational.logarithm_storageBits line 86
  17. def OAI.EditApproximation.UnreducedRational.optimizerStep line 96
  18. def OAI.EditApproximation.UnreducedRational.optimizerIterate line 98
  19. theorem OAI.EditApproximation.UnreducedRational.optimizerStep_value line 104
  20. theorem OAI.EditApproximation.UnreducedRational.optimizerIterate_value line 108
  21. theorem OAI.EditApproximation.UnreducedRational.optimizerStep_den line 116
  22. theorem OAI.EditApproximation.UnreducedRational.optimizerIterate_den_bits line 121