OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseOneXAllPrecision.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptCase1X0Interval line 12
  2. theorem OAI.InternalCatalan.manuscript_case1X0_interval line 17
  3. theorem OAI.InternalCatalan.manuscript_case1X0_endpoint_lt_printed line 23
  4. theorem OAI.InternalCatalan.manuscript_case1X0_interval_width line 31
  5. theorem OAI.InternalCatalan.manuscript_case1X0_printed_upper line 40
  6. def OAI.InternalCatalan.manuscriptCase1X1Interval line 57
  7. theorem OAI.InternalCatalan.manuscript_case1X1_interval line 60
  8. theorem OAI.InternalCatalan.manuscript_case1X1_endpoint_lt_printed line 64
  9. theorem OAI.InternalCatalan.manuscript_case1X1_interval_width line 72
  10. theorem OAI.InternalCatalan.manuscript_case1X1_printed_upper line 80
  11. def OAI.InternalCatalan.manuscriptCase1X2Interval line 97
  12. theorem OAI.InternalCatalan.manuscript_case1X2_interval line 100
  13. theorem OAI.InternalCatalan.manuscript_case1X2_endpoint_lt_printed line 104
  14. theorem OAI.InternalCatalan.manuscript_case1X2_interval_width line 112
  15. theorem OAI.InternalCatalan.manuscript_case1X2_printed_upper line 120
  16. def OAI.InternalCatalan.manuscriptCase1X3Interval line 137
  17. theorem OAI.InternalCatalan.manuscript_case1X3_interval line 140
  18. theorem OAI.InternalCatalan.manuscript_case1X3_endpoint_lt_printed line 144
  19. theorem OAI.InternalCatalan.manuscript_case1X3_interval_width line 152
  20. theorem OAI.InternalCatalan.manuscript_case1X3_printed_upper line 160
  21. def OAI.InternalCatalan.manuscriptCase1X4Interval line 177
  22. theorem OAI.InternalCatalan.manuscript_case1X4_interval line 180
  23. theorem OAI.InternalCatalan.manuscript_case1X4_endpoint_lt_printed line 184
  24. theorem OAI.InternalCatalan.manuscript_case1X4_interval_width line 192
  25. theorem OAI.InternalCatalan.manuscript_case1X4_printed_upper line 200
  26. def OAI.InternalCatalan.manuscriptCase1X5Interval line 217
  27. theorem OAI.InternalCatalan.manuscript_case1X5_interval line 220
  28. theorem OAI.InternalCatalan.manuscript_case1X5_endpoint_lt_printed line 224
  29. theorem OAI.InternalCatalan.manuscript_case1X5_interval_width line 232
  30. theorem OAI.InternalCatalan.manuscript_case1X5_printed_upper line 240
  31. def OAI.InternalCatalan.manuscriptCase1X6Interval line 257
  32. theorem OAI.InternalCatalan.manuscript_case1X6_interval line 260
  33. theorem OAI.InternalCatalan.manuscript_case1X6_endpoint_lt_printed line 264
  34. theorem OAI.InternalCatalan.manuscript_case1X6_interval_width line 272
  35. theorem OAI.InternalCatalan.manuscript_case1X6_printed_upper line 280
  36. def OAI.InternalCatalan.manuscriptCase1X7Interval line 297
  37. theorem OAI.InternalCatalan.manuscript_case1X7_interval line 300
  38. theorem OAI.InternalCatalan.manuscript_case1X7_endpoint_lt_printed line 304
  39. theorem OAI.InternalCatalan.manuscript_case1X7_interval_width line 312
  40. theorem OAI.InternalCatalan.manuscript_case1X7_printed_upper line 320
  41. def OAI.InternalCatalan.manuscriptCase1XPrecisionClaims line 336
  42. theorem OAI.InternalCatalan.manuscript_case1X_all_precision line 370