OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseTwoY14SubstitutionError.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptCase2Y14FieldInterval line 14
  2. theorem OAI.InternalCatalan.manuscriptCase2Y14_field_rounded line 17
  3. theorem OAI.InternalCatalan.manuscriptCase2Y14_YV_tail_eq line 26
  4. def OAI.InternalCatalan.manuscriptCase2Y14Interval line 47
  5. theorem OAI.InternalCatalan.manuscript_case2Y14_interval line 51
  6. theorem OAI.InternalCatalan.manuscript_case2Y14_rounded_endpoints line 86
  7. def OAI.InternalCatalan.manuscriptCase2Y14PrintedUpper line 112
  8. theorem OAI.InternalCatalan.manuscript_case2Y14_endpoint_lt_printed line 114
  9. theorem OAI.InternalCatalan.manuscript_case2Y14_interval_width line 118
  10. theorem OAI.InternalCatalan.manuscript_case2Y14_printed_upper line 123
  11. def OAI.InternalCatalan.manuscriptCase2Y14SubstituteRat line 139
  12. theorem OAI.InternalCatalan.manuscript_case2Y14_substitute_interval line 155
  13. theorem OAI.InternalCatalan.manuscript_case2Y14_substitute_cutoff line 189
  14. def OAI.InternalCatalan.manuscriptCase2Y14RoundedSubstituteRat line 206
  15. theorem OAI.InternalCatalan.manuscript_case2Y14_additional_rounding_error line 222
  16. theorem OAI.InternalCatalan.manuscript_case2Y14_actual_substitution_error line 323