OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX9.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2X9XV0LogArg line 10
  2. theorem OAI.InternalCatalan.barrierCase2X9XV0_arg_eq line 13
  3. theorem OAI.InternalCatalan.barrierCase2X9XV0_arg_regular line 19
  4. theorem OAI.InternalCatalan.barrierCase2X9XV0_weight_eq line 24
  5. theorem OAI.InternalCatalan.barrierCase2X9XV0_error line 29
  6. theorem OAI.InternalCatalan.barrierCase2X9XV0_approx_upper line 44
  7. theorem OAI.InternalCatalan.barrierCase2X9XV0_log_upper line 51
  8. def OAI.InternalCatalan.barrierCase2X9XV1LogArg line 62
  9. theorem OAI.InternalCatalan.barrierCase2X9XV1_arg_eq line 65
  10. theorem OAI.InternalCatalan.barrierCase2X9XV1_arg_regular line 71
  11. theorem OAI.InternalCatalan.barrierCase2X9XV1_weight_eq line 76
  12. theorem OAI.InternalCatalan.barrierCase2X9XV1_error line 81
  13. theorem OAI.InternalCatalan.barrierCase2X9XV1_approx_upper line 96
  14. theorem OAI.InternalCatalan.barrierCase2X9XV1_log_upper line 103
  15. def OAI.InternalCatalan.barrierCase2X9XV2LogArg line 114
  16. theorem OAI.InternalCatalan.barrierCase2X9XV2_arg_eq line 117
  17. theorem OAI.InternalCatalan.barrierCase2X9XV2_arg_regular line 123
  18. theorem OAI.InternalCatalan.barrierCase2X9XV2_weight_eq line 128
  19. theorem OAI.InternalCatalan.barrierCase2X9XV2_error line 133
  20. theorem OAI.InternalCatalan.barrierCase2X9XV2_approx_upper line 148
  21. theorem OAI.InternalCatalan.barrierCase2X9XV2_log_upper line 155
  22. def OAI.InternalCatalan.barrierCase2X9XV3LogArg line 166
  23. theorem OAI.InternalCatalan.barrierCase2X9XV3_arg_eq line 169
  24. theorem OAI.InternalCatalan.barrierCase2X9XV3_arg_regular line 175
  25. theorem OAI.InternalCatalan.barrierCase2X9XV3_weight_eq line 180
  26. theorem OAI.InternalCatalan.barrierCase2X9XV3_error line 185
  27. theorem OAI.InternalCatalan.barrierCase2X9XV3_approx_upper line 200
  28. theorem OAI.InternalCatalan.barrierCase2X9XV3_log_upper line 207
  29. def OAI.InternalCatalan.barrierCase2X9XV4LogArg line 218
  30. theorem OAI.InternalCatalan.barrierCase2X9XV4_arg_eq line 221
  31. theorem OAI.InternalCatalan.barrierCase2X9XV4_arg_regular line 227
  32. theorem OAI.InternalCatalan.barrierCase2X9XV4_weight_eq line 232
  33. theorem OAI.InternalCatalan.barrierCase2X9XV4_error line 237
  34. theorem OAI.InternalCatalan.barrierCase2X9XV4_approx_upper line 252
  35. theorem OAI.InternalCatalan.barrierCase2X9XV4_log_upper line 259
  36. def OAI.InternalCatalan.barrierCase2X9XV5LogArg line 270
  37. theorem OAI.InternalCatalan.barrierCase2X9XV5_arg_eq line 273
  38. theorem OAI.InternalCatalan.barrierCase2X9XV5_arg_regular line 279
  39. theorem OAI.InternalCatalan.barrierCase2X9XV5_weight_eq line 284
  40. theorem OAI.InternalCatalan.barrierCase2X9XV5_error line 289
  41. theorem OAI.InternalCatalan.barrierCase2X9XV5_approx_upper line 304
  42. theorem OAI.InternalCatalan.barrierCase2X9XV5_log_upper line 311
  43. def OAI.InternalCatalan.barrierCase2X9XV7LogArg line 327
  44. theorem OAI.InternalCatalan.barrierCase2X9XV7_arg_eq line 330
  45. theorem OAI.InternalCatalan.barrierCase2X9XV7_arg_regular line 336
  46. theorem OAI.InternalCatalan.barrierCase2X9XV7_weight_eq line 341
  47. theorem OAI.InternalCatalan.barrierCase2X9XV7_error line 346
  48. theorem OAI.InternalCatalan.barrierCase2X9XV7_approx_upper line 361
  49. theorem OAI.InternalCatalan.barrierCase2X9XV7_log_upper line 368
  50. def OAI.InternalCatalan.barrierCase2X9XV9LogArg line 379
  51. theorem OAI.InternalCatalan.barrierCase2X9XV9_arg_eq line 382
  52. theorem OAI.InternalCatalan.barrierCase2X9XV9_arg_regular line 388
  53. theorem OAI.InternalCatalan.barrierCase2X9XV9_weight_eq line 393
  54. theorem OAI.InternalCatalan.barrierCase2X9XV9_error line 398
  55. theorem OAI.InternalCatalan.barrierCase2X9XV9_approx_upper line 413
  56. theorem OAI.InternalCatalan.barrierCase2X9XV9_log_upper line 420
  57. def OAI.InternalCatalan.barrierCase2X9XV11LogArg line 431
  58. theorem OAI.InternalCatalan.barrierCase2X9XV11_arg_eq line 434
  59. theorem OAI.InternalCatalan.barrierCase2X9XV11_arg_regular line 440
  60. theorem OAI.InternalCatalan.barrierCase2X9XV11_weight_eq line 445
  61. theorem OAI.InternalCatalan.barrierCase2X9XV11_error line 450
  62. theorem OAI.InternalCatalan.barrierCase2X9XV11_approx_upper line 465
  63. theorem OAI.InternalCatalan.barrierCase2X9XV11_log_upper line 472
  64. theorem OAI.InternalCatalan.barrierCase2X9_XP_tail_upper line 489
  65. theorem OAI.InternalCatalan.barrierCase2X9_XV_tail_upper line 511
  66. theorem OAI.InternalCatalan.barrierCase2X9_approx_upper line 536
  67. theorem OAI.InternalCatalan.barrierCase2X9_lt line 544