OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseTwoX13SubstitutionError.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptCase2X13FieldInterval line 16
  2. theorem OAI.InternalCatalan.manuscriptCase2X13_field_rounded line 19
  3. theorem OAI.InternalCatalan.manuscriptCase2X13_XP_tail_eq line 28
  4. theorem OAI.InternalCatalan.manuscriptCase2X13_XV_tail_eq line 46
  5. def OAI.InternalCatalan.manuscriptCase2X13Interval line 67
  6. theorem OAI.InternalCatalan.manuscript_case2X13_interval line 71
  7. theorem OAI.InternalCatalan.manuscript_case2X13_rounded_endpoints line 119
  8. def OAI.InternalCatalan.manuscriptCase2X13PrintedUpper line 157
  9. theorem OAI.InternalCatalan.manuscript_case2X13_endpoint_lt_printed line 159
  10. theorem OAI.InternalCatalan.manuscript_case2X13_interval_width line 163
  11. theorem OAI.InternalCatalan.manuscript_case2X13_printed_upper line 168
  12. def OAI.InternalCatalan.manuscriptCase2X13SubstituteRat line 184
  13. theorem OAI.InternalCatalan.manuscript_case2X13_substitute_interval line 210
  14. theorem OAI.InternalCatalan.manuscript_case2X13_substitute_cutoff line 260
  15. def OAI.InternalCatalan.manuscriptCase2X13RoundedSubstituteRat line 277
  16. theorem OAI.InternalCatalan.manuscript_case2X13_additional_rounding_error line 303
  17. theorem OAI.InternalCatalan.manuscript_case2X13_actual_substitution_error line 464