OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX0.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrier_T_3 line 15

    Also declared: OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean:12 (same declaration text).

  2. theorem OAI.InternalCatalan.barrier_T_4 line 19

    Also declared: OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean:16 (same declaration text).

  3. theorem OAI.InternalCatalan.barrier_T_5 line 23

    Also declared: OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean:20 (same declaration text).

  4. theorem OAI.InternalCatalan.barrier_T_6 line 27

    Also declared: OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean:24 (same declaration text).

  5. theorem OAI.InternalCatalan.barrier_T_7 line 31

    Also declared: OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean:28 (same declaration text).

  6. theorem OAI.InternalCatalan.barrier_T_8 line 35

    Also declared: OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointY1.lean:32 (same declaration text).

  7. theorem OAI.InternalCatalan.barrier_T_9 line 39
  8. theorem OAI.InternalCatalan.barrier_T_10 line 43
  9. def OAI.InternalCatalan.barrierCase2TPExplicit line 47
  10. theorem OAI.InternalCatalan.barrierCase2TP_eq_explicit line 60
  11. def OAI.InternalCatalan.barrierCase2TVExplicit line 67
  12. theorem OAI.InternalCatalan.barrierCase2TV_eq_explicit line 80
  13. def OAI.InternalCatalan.barrierCase2SVExplicit line 87
  14. theorem OAI.InternalCatalan.barrierCase2SV_eq_explicit line 99
  15. def OAI.InternalCatalan.barrierCase2X0XV0LogArg line 108
  16. theorem OAI.InternalCatalan.barrierCase2X0XV0_arg_eq line 111
  17. theorem OAI.InternalCatalan.barrierCase2X0XV0_arg_regular line 117
  18. theorem OAI.InternalCatalan.barrierCase2X0XV0_weight_eq line 122
  19. theorem OAI.InternalCatalan.barrierCase2X0XV0_error line 127
  20. theorem OAI.InternalCatalan.barrierCase2X0XV0_approx_upper line 142
  21. theorem OAI.InternalCatalan.barrierCase2X0XV0_log_upper line 149
  22. def OAI.InternalCatalan.barrierCase2X0XV1LogArg line 160
  23. theorem OAI.InternalCatalan.barrierCase2X0XV1_arg_eq line 163
  24. theorem OAI.InternalCatalan.barrierCase2X0XV1_arg_regular line 169
  25. theorem OAI.InternalCatalan.barrierCase2X0XV1_weight_eq line 174
  26. theorem OAI.InternalCatalan.barrierCase2X0XV1_error line 179
  27. theorem OAI.InternalCatalan.barrierCase2X0XV1_approx_upper line 194
  28. theorem OAI.InternalCatalan.barrierCase2X0XV1_log_upper line 201
  29. def OAI.InternalCatalan.barrierCase2X0XV2LogArg line 212
  30. theorem OAI.InternalCatalan.barrierCase2X0XV2_arg_eq line 215
  31. theorem OAI.InternalCatalan.barrierCase2X0XV2_arg_regular line 221
  32. theorem OAI.InternalCatalan.barrierCase2X0XV2_weight_eq line 226
  33. theorem OAI.InternalCatalan.barrierCase2X0XV2_error line 231
  34. theorem OAI.InternalCatalan.barrierCase2X0XV2_approx_upper line 246
  35. theorem OAI.InternalCatalan.barrierCase2X0XV2_log_upper line 253
  36. def OAI.InternalCatalan.barrierCase2X0XV3LogArg line 264
  37. theorem OAI.InternalCatalan.barrierCase2X0XV3_arg_eq line 267
  38. theorem OAI.InternalCatalan.barrierCase2X0XV3_arg_regular line 273
  39. theorem OAI.InternalCatalan.barrierCase2X0XV3_weight_eq line 278
  40. theorem OAI.InternalCatalan.barrierCase2X0XV3_error line 283
  41. theorem OAI.InternalCatalan.barrierCase2X0XV3_approx_upper line 298
  42. theorem OAI.InternalCatalan.barrierCase2X0XV3_log_upper line 305
  43. def OAI.InternalCatalan.barrierCase2X0XV4LogArg line 316
  44. theorem OAI.InternalCatalan.barrierCase2X0XV4_arg_eq line 319
  45. theorem OAI.InternalCatalan.barrierCase2X0XV4_arg_regular line 325
  46. theorem OAI.InternalCatalan.barrierCase2X0XV4_weight_eq line 330
  47. theorem OAI.InternalCatalan.barrierCase2X0XV4_error line 335
  48. theorem OAI.InternalCatalan.barrierCase2X0XV4_approx_upper line 350
  49. theorem OAI.InternalCatalan.barrierCase2X0XV4_log_upper line 357
  50. def OAI.InternalCatalan.barrierCase2X0XV5LogArg line 368
  51. theorem OAI.InternalCatalan.barrierCase2X0XV5_arg_eq line 371
  52. theorem OAI.InternalCatalan.barrierCase2X0XV5_arg_regular line 377
  53. theorem OAI.InternalCatalan.barrierCase2X0XV5_weight_eq line 382
  54. theorem OAI.InternalCatalan.barrierCase2X0XV5_error line 387
  55. theorem OAI.InternalCatalan.barrierCase2X0XV5_approx_upper line 402
  56. theorem OAI.InternalCatalan.barrierCase2X0XV5_log_upper line 409
  57. def OAI.InternalCatalan.barrierCase2X0XV7LogArg line 420
  58. theorem OAI.InternalCatalan.barrierCase2X0XV7_arg_eq line 423
  59. theorem OAI.InternalCatalan.barrierCase2X0XV7_arg_regular line 429
  60. theorem OAI.InternalCatalan.barrierCase2X0XV7_weight_eq line 434
  61. theorem OAI.InternalCatalan.barrierCase2X0XV7_error line 439
  62. theorem OAI.InternalCatalan.barrierCase2X0XV7_approx_upper line 454
  63. theorem OAI.InternalCatalan.barrierCase2X0XV7_log_upper line 461
  64. def OAI.InternalCatalan.barrierCase2X0XV9LogArg line 472
  65. theorem OAI.InternalCatalan.barrierCase2X0XV9_arg_eq line 475
  66. theorem OAI.InternalCatalan.barrierCase2X0XV9_arg_regular line 481
  67. theorem OAI.InternalCatalan.barrierCase2X0XV9_weight_eq line 486
  68. theorem OAI.InternalCatalan.barrierCase2X0XV9_error line 491
  69. theorem OAI.InternalCatalan.barrierCase2X0XV9_approx_upper line 506
  70. theorem OAI.InternalCatalan.barrierCase2X0XV9_log_upper line 513
  71. def OAI.InternalCatalan.barrierCase2X0XV11LogArg line 524
  72. theorem OAI.InternalCatalan.barrierCase2X0XV11_arg_eq line 527
  73. theorem OAI.InternalCatalan.barrierCase2X0XV11_arg_regular line 533
  74. theorem OAI.InternalCatalan.barrierCase2X0XV11_weight_eq line 538
  75. theorem OAI.InternalCatalan.barrierCase2X0XV11_error line 543
  76. theorem OAI.InternalCatalan.barrierCase2X0XV11_approx_upper line 558
  77. theorem OAI.InternalCatalan.barrierCase2X0XV11_log_upper line 565
  78. theorem OAI.InternalCatalan.barrierCase2X0_XP_tail_upper line 578
  79. theorem OAI.InternalCatalan.barrierCase2X0_XV_tail_upper line 600
  80. theorem OAI.InternalCatalan.barrierCase2X0_approx_upper line 625
  81. theorem OAI.InternalCatalan.barrierCase2X0_lt line 633