OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoGlobalBounds.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2Y9YV0LogArg line 44
  2. theorem OAI.InternalCatalan.barrierCase2Y9YV0_arg_eq line 47
  3. theorem OAI.InternalCatalan.barrierCase2Y9YV0_arg_regular line 53
  4. theorem OAI.InternalCatalan.barrierCase2Y9YV0_weight_eq line 58
  5. theorem OAI.InternalCatalan.barrierCase2Y9YV0_error line 63
  6. theorem OAI.InternalCatalan.barrierCase2Y9YV0_approx_upper line 78
  7. theorem OAI.InternalCatalan.barrierCase2Y9YV0_log_upper line 85
  8. def OAI.InternalCatalan.barrierCase2Y9YV1LogArg line 96
  9. theorem OAI.InternalCatalan.barrierCase2Y9YV1_arg_eq line 99
  10. theorem OAI.InternalCatalan.barrierCase2Y9YV1_arg_regular line 105
  11. theorem OAI.InternalCatalan.barrierCase2Y9YV1_weight_eq line 110
  12. theorem OAI.InternalCatalan.barrierCase2Y9YV1_error line 115
  13. theorem OAI.InternalCatalan.barrierCase2Y9YV1_approx_upper line 130
  14. theorem OAI.InternalCatalan.barrierCase2Y9YV1_log_upper line 137
  15. def OAI.InternalCatalan.barrierCase2Y9YV2LogArg line 148
  16. theorem OAI.InternalCatalan.barrierCase2Y9YV2_arg_eq line 151
  17. theorem OAI.InternalCatalan.barrierCase2Y9YV2_arg_regular line 157
  18. theorem OAI.InternalCatalan.barrierCase2Y9YV2_weight_eq line 162
  19. theorem OAI.InternalCatalan.barrierCase2Y9YV2_error line 167
  20. theorem OAI.InternalCatalan.barrierCase2Y9YV2_approx_upper line 182
  21. theorem OAI.InternalCatalan.barrierCase2Y9YV2_log_upper line 189
  22. def OAI.InternalCatalan.barrierCase2Y9YV3LogArg line 200
  23. theorem OAI.InternalCatalan.barrierCase2Y9YV3_arg_eq line 203
  24. theorem OAI.InternalCatalan.barrierCase2Y9YV3_arg_regular line 209
  25. theorem OAI.InternalCatalan.barrierCase2Y9YV3_weight_eq line 214
  26. theorem OAI.InternalCatalan.barrierCase2Y9YV3_error line 219
  27. theorem OAI.InternalCatalan.barrierCase2Y9YV3_approx_upper line 234
  28. theorem OAI.InternalCatalan.barrierCase2Y9YV3_log_upper line 241
  29. def OAI.InternalCatalan.barrierCase2Y9YV4LogArg line 252
  30. theorem OAI.InternalCatalan.barrierCase2Y9YV4_arg_eq line 255
  31. theorem OAI.InternalCatalan.barrierCase2Y9YV4_arg_regular line 261
  32. theorem OAI.InternalCatalan.barrierCase2Y9YV4_weight_eq line 266
  33. theorem OAI.InternalCatalan.barrierCase2Y9YV4_error line 271
  34. theorem OAI.InternalCatalan.barrierCase2Y9YV4_approx_upper line 286
  35. theorem OAI.InternalCatalan.barrierCase2Y9YV4_log_upper line 293
  36. def OAI.InternalCatalan.barrierCase2Y9YV5LogArg line 304
  37. theorem OAI.InternalCatalan.barrierCase2Y9YV5_arg_eq line 307
  38. theorem OAI.InternalCatalan.barrierCase2Y9YV5_arg_regular line 313
  39. theorem OAI.InternalCatalan.barrierCase2Y9YV5_weight_eq line 318
  40. theorem OAI.InternalCatalan.barrierCase2Y9YV5_error line 323
  41. theorem OAI.InternalCatalan.barrierCase2Y9YV5_approx_upper line 338
  42. theorem OAI.InternalCatalan.barrierCase2Y9YV5_log_upper line 345
  43. def OAI.InternalCatalan.barrierCase2Y9YV7LogArg line 361
  44. theorem OAI.InternalCatalan.barrierCase2Y9YV7_arg_eq line 364
  45. theorem OAI.InternalCatalan.barrierCase2Y9YV7_arg_regular line 370
  46. theorem OAI.InternalCatalan.barrierCase2Y9YV7_weight_eq line 375
  47. theorem OAI.InternalCatalan.barrierCase2Y9YV7_error line 380
  48. theorem OAI.InternalCatalan.barrierCase2Y9YV7_approx_upper line 395
  49. theorem OAI.InternalCatalan.barrierCase2Y9YV7_log_upper line 402
  50. def OAI.InternalCatalan.barrierCase2Y9YV9LogArg line 413
  51. theorem OAI.InternalCatalan.barrierCase2Y9YV9_arg_eq line 416
  52. theorem OAI.InternalCatalan.barrierCase2Y9YV9_arg_regular line 422
  53. theorem OAI.InternalCatalan.barrierCase2Y9YV9_weight_eq line 427
  54. theorem OAI.InternalCatalan.barrierCase2Y9YV9_error line 432
  55. theorem OAI.InternalCatalan.barrierCase2Y9YV9_approx_upper line 447
  56. theorem OAI.InternalCatalan.barrierCase2Y9YV9_log_upper line 454
  57. def OAI.InternalCatalan.barrierCase2Y9YV11LogArg line 465
  58. theorem OAI.InternalCatalan.barrierCase2Y9YV11_arg_eq line 468
  59. theorem OAI.InternalCatalan.barrierCase2Y9YV11_arg_regular line 474
  60. theorem OAI.InternalCatalan.barrierCase2Y9YV11_weight_eq line 479
  61. theorem OAI.InternalCatalan.barrierCase2Y9YV11_error line 484
  62. theorem OAI.InternalCatalan.barrierCase2Y9YV11_approx_upper line 499
  63. theorem OAI.InternalCatalan.barrierCase2Y9YV11_log_upper line 506
  64. theorem OAI.InternalCatalan.barrierCase2Y9_YV_tail_upper line 523
  65. theorem OAI.InternalCatalan.barrierCase2Y9_approx_upper line 548
  66. theorem OAI.InternalCatalan.barrierCase2Y9_lt line 556
  67. theorem OAI.InternalCatalan.barrierCase2X_bracket_left_lt line 573
  68. theorem OAI.InternalCatalan.barrierCase2Y_bracket_left_lt line 615
  69. theorem OAI.InternalCatalan.barrierCase2X_neg_one_lt line 651
  70. theorem OAI.InternalCatalan.barrierCase2X_global_upper line 659
  71. theorem OAI.InternalCatalan.barrierCase2Y_global_upper line 676