OAI/Combinatorics/EditApproximation/Numerics/RationalIntermediateBits.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounds on the reduced integer representations produced by the rational operations in the materialized numerical routines.

  1. theorem OAI.EditApproximation.rational_add_numerator_le line 10
  2. theorem OAI.EditApproximation.rational_mul_numerator_le line 21
  3. theorem OAI.EditApproximation.rationalEncodingBits_add line 30
  4. theorem OAI.EditApproximation.rationalEncodingBits_mul line 41
  5. theorem OAI.EditApproximation.rationalEncodingBits_neg line 50
  6. theorem OAI.EditApproximation.rationalEncodingBits_sub line 53
  7. theorem OAI.EditApproximation.rationalEncodingBits_inv line 57
  8. theorem OAI.EditApproximation.rationalEncodingBits_div line 67
  9. theorem OAI.EditApproximation.rationalEncodingBits_natCast line 74
  10. theorem OAI.EditApproximation.rationalEncodingBits_pow line 78