OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseOneY0PointRounding.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptCase1Y0Interval line 11
  2. theorem OAI.InternalCatalan.manuscript_case1Y0_interval line 14
  3. theorem OAI.InternalCatalan.manuscript_case1Y0_endpoint_lt_printed line 18
  4. theorem OAI.InternalCatalan.manuscript_case1Y0_interval_width line 26
  5. theorem OAI.InternalCatalan.manuscript_case1Y0_printed_upper line 34
  6. def OAI.InternalCatalan.manuscriptCase1Y1Interval line 51
  7. theorem OAI.InternalCatalan.manuscript_case1Y1_interval line 54
  8. theorem OAI.InternalCatalan.manuscript_case1Y1_endpoint_lt_printed line 58
  9. theorem OAI.InternalCatalan.manuscript_case1Y1_interval_width line 66
  10. theorem OAI.InternalCatalan.manuscript_case1Y1_printed_upper line 74
  11. def OAI.InternalCatalan.manuscriptCase1Y2Interval line 91
  12. theorem OAI.InternalCatalan.manuscript_case1Y2_interval line 94
  13. theorem OAI.InternalCatalan.manuscript_case1Y2_endpoint_lt_printed line 98
  14. theorem OAI.InternalCatalan.manuscript_case1Y2_interval_width line 106
  15. theorem OAI.InternalCatalan.manuscript_case1Y2_printed_upper line 114
  16. def OAI.InternalCatalan.manuscriptCase1Y3Interval line 131
  17. theorem OAI.InternalCatalan.manuscript_case1Y3_interval line 134
  18. theorem OAI.InternalCatalan.manuscript_case1Y3_endpoint_lt_printed line 138
  19. theorem OAI.InternalCatalan.manuscript_case1Y3_interval_width line 146
  20. theorem OAI.InternalCatalan.manuscript_case1Y3_printed_upper line 154
  21. def OAI.InternalCatalan.manuscriptCase1Y4Interval line 171
  22. theorem OAI.InternalCatalan.manuscript_case1Y4_interval line 174
  23. theorem OAI.InternalCatalan.manuscript_case1Y4_endpoint_lt_printed line 178
  24. theorem OAI.InternalCatalan.manuscript_case1Y4_interval_width line 186
  25. theorem OAI.InternalCatalan.manuscript_case1Y4_printed_upper line 194
  26. def OAI.InternalCatalan.manuscriptCase1YPrecisionClaims line 210
  27. theorem OAI.InternalCatalan.manuscript_case1Y_all_precision line 232
  28. def OAI.InternalCatalan.manuscriptCase1Y0SubstituteRat line 251
  29. theorem OAI.InternalCatalan.manuscript_case1Y0_substitute_interval line 254
  30. theorem OAI.InternalCatalan.manuscript_case1Y0_substitute_cutoff line 260
  31. def OAI.InternalCatalan.manuscriptCase1Y1SubstituteRat line 277
  32. theorem OAI.InternalCatalan.manuscript_case1Y1_substitute_interval line 280
  33. theorem OAI.InternalCatalan.manuscript_case1Y1_substitute_cutoff line 286
  34. def OAI.InternalCatalan.manuscriptCase1Y2SubstituteRat line 303
  35. theorem OAI.InternalCatalan.manuscript_case1Y2_substitute_interval line 306
  36. theorem OAI.InternalCatalan.manuscript_case1Y2_substitute_cutoff line 312
  37. def OAI.InternalCatalan.manuscriptCase1Y3SubstituteRat line 329
  38. theorem OAI.InternalCatalan.manuscript_case1Y3_substitute_interval line 332
  39. theorem OAI.InternalCatalan.manuscript_case1Y3_substitute_cutoff line 338
  40. def OAI.InternalCatalan.manuscriptCase1Y4SubstituteRat line 355
  41. theorem OAI.InternalCatalan.manuscript_case1Y4_substitute_interval line 358
  42. theorem OAI.InternalCatalan.manuscript_case1Y4_substitute_cutoff line 364
  43. def OAI.InternalCatalan.manuscriptCase1Y0RoundedSubstituteRat line 381
  44. theorem OAI.InternalCatalan.manuscript_case1Y0_additional_rounding_error line 384