OAI/NumberTheory/Catalan/Estimates/ManuscriptAllFiftyPointPrecision.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptCase2X9FieldInterval line 35
  2. theorem OAI.InternalCatalan.manuscriptCase2X9_field_rounded line 38
  3. theorem OAI.InternalCatalan.manuscriptCase2X9_XP_tail_eq line 47
  4. theorem OAI.InternalCatalan.manuscriptCase2X9_XV_tail_eq line 65
  5. def OAI.InternalCatalan.manuscriptCase2X9Interval line 86
  6. theorem OAI.InternalCatalan.manuscript_case2X9_interval line 90
  7. theorem OAI.InternalCatalan.manuscript_case2X9_rounded_endpoints line 138
  8. def OAI.InternalCatalan.manuscriptCase2X9PrintedUpper line 176
  9. theorem OAI.InternalCatalan.manuscript_case2X9_endpoint_lt_printed line 178
  10. theorem OAI.InternalCatalan.manuscript_case2X9_interval_width line 182
  11. theorem OAI.InternalCatalan.manuscript_case2X9_printed_upper line 187
  12. def OAI.InternalCatalan.manuscriptCase2X9SubstituteRat line 203
  13. theorem OAI.InternalCatalan.manuscript_case2X9_substitute_interval line 229
  14. theorem OAI.InternalCatalan.manuscript_case2X9_substitute_cutoff line 279
  15. def OAI.InternalCatalan.manuscriptCase2XPrecisionClaims line 295
  16. theorem OAI.InternalCatalan.manuscript_case2X_all_precision line 373
  17. def OAI.InternalCatalan.manuscriptCase2X9RoundedSubstituteRat line 406
  18. theorem OAI.InternalCatalan.manuscript_case2X9_additional_rounding_error line 432
  19. theorem OAI.InternalCatalan.manuscript_case2X9_actual_substitution_error line 593
  20. theorem OAI.InternalCatalan.manuscript_all_fifty_point_precision line 612