OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseTwoYAllPrecision.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptCase2Y8FieldInterval line 32
  2. theorem OAI.InternalCatalan.manuscriptCase2Y8_field_rounded line 35
  3. theorem OAI.InternalCatalan.manuscriptCase2Y8_YV_tail_eq line 44
  4. def OAI.InternalCatalan.manuscriptCase2Y8Interval line 65
  5. theorem OAI.InternalCatalan.manuscript_case2Y8_interval line 69
  6. theorem OAI.InternalCatalan.manuscript_case2Y8_rounded_endpoints line 104
  7. def OAI.InternalCatalan.manuscriptCase2Y8PrintedUpper line 130
  8. theorem OAI.InternalCatalan.manuscript_case2Y8_endpoint_lt_printed line 132
  9. theorem OAI.InternalCatalan.manuscript_case2Y8_interval_width line 136
  10. theorem OAI.InternalCatalan.manuscript_case2Y8_printed_upper line 141
  11. def OAI.InternalCatalan.manuscriptCase2Y9FieldInterval line 157
  12. theorem OAI.InternalCatalan.manuscriptCase2Y9_field_rounded line 160
  13. theorem OAI.InternalCatalan.manuscriptCase2Y9_YV_tail_eq line 169
  14. def OAI.InternalCatalan.manuscriptCase2Y9Interval line 190
  15. theorem OAI.InternalCatalan.manuscript_case2Y9_interval line 194
  16. theorem OAI.InternalCatalan.manuscript_case2Y9_rounded_endpoints line 229
  17. def OAI.InternalCatalan.manuscriptCase2Y9PrintedUpper line 255
  18. theorem OAI.InternalCatalan.manuscript_case2Y9_endpoint_lt_printed line 257
  19. theorem OAI.InternalCatalan.manuscript_case2Y9_interval_width line 261
  20. theorem OAI.InternalCatalan.manuscript_case2Y9_printed_upper line 266
  21. def OAI.InternalCatalan.manuscriptCase2Y8SubstituteRat line 282
  22. theorem OAI.InternalCatalan.manuscript_case2Y8_substitute_interval line 298
  23. theorem OAI.InternalCatalan.manuscript_case2Y8_substitute_cutoff line 332
  24. def OAI.InternalCatalan.manuscriptCase2Y9SubstituteRat line 349
  25. theorem OAI.InternalCatalan.manuscript_case2Y9_substitute_interval line 365
  26. theorem OAI.InternalCatalan.manuscript_case2Y9_substitute_cutoff line 399
  27. def OAI.InternalCatalan.manuscriptCase2YPrecisionClaims line 415
  28. theorem OAI.InternalCatalan.manuscript_case2Y_all_precision line 489