OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointX2.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2X2XV0LogArg line 10
  2. theorem OAI.InternalCatalan.barrierCase2X2XV0_arg_eq line 13
  3. theorem OAI.InternalCatalan.barrierCase2X2XV0_arg_regular line 19
  4. theorem OAI.InternalCatalan.barrierCase2X2XV0_weight_eq line 24
  5. theorem OAI.InternalCatalan.barrierCase2X2XV0_error line 29
  6. theorem OAI.InternalCatalan.barrierCase2X2XV0_approx_upper line 44
  7. theorem OAI.InternalCatalan.barrierCase2X2XV0_log_upper line 51
  8. def OAI.InternalCatalan.barrierCase2X2XV1LogArg line 62
  9. theorem OAI.InternalCatalan.barrierCase2X2XV1_arg_eq line 65
  10. theorem OAI.InternalCatalan.barrierCase2X2XV1_arg_regular line 71
  11. theorem OAI.InternalCatalan.barrierCase2X2XV1_weight_eq line 76
  12. theorem OAI.InternalCatalan.barrierCase2X2XV1_error line 81
  13. theorem OAI.InternalCatalan.barrierCase2X2XV1_approx_upper line 96
  14. theorem OAI.InternalCatalan.barrierCase2X2XV1_log_upper line 103
  15. def OAI.InternalCatalan.barrierCase2X2XV2LogArg line 114
  16. theorem OAI.InternalCatalan.barrierCase2X2XV2_arg_eq line 117
  17. theorem OAI.InternalCatalan.barrierCase2X2XV2_arg_regular line 123
  18. theorem OAI.InternalCatalan.barrierCase2X2XV2_weight_eq line 128
  19. theorem OAI.InternalCatalan.barrierCase2X2XV2_error line 133
  20. theorem OAI.InternalCatalan.barrierCase2X2XV2_approx_upper line 148
  21. theorem OAI.InternalCatalan.barrierCase2X2XV2_log_upper line 155
  22. def OAI.InternalCatalan.barrierCase2X2XV3LogArg line 166
  23. theorem OAI.InternalCatalan.barrierCase2X2XV3_arg_eq line 169
  24. theorem OAI.InternalCatalan.barrierCase2X2XV3_arg_regular line 175
  25. theorem OAI.InternalCatalan.barrierCase2X2XV3_weight_eq line 180
  26. theorem OAI.InternalCatalan.barrierCase2X2XV3_error line 185
  27. theorem OAI.InternalCatalan.barrierCase2X2XV3_approx_upper line 200
  28. theorem OAI.InternalCatalan.barrierCase2X2XV3_log_upper line 207
  29. def OAI.InternalCatalan.barrierCase2X2XV4LogArg line 218
  30. theorem OAI.InternalCatalan.barrierCase2X2XV4_arg_eq line 221
  31. theorem OAI.InternalCatalan.barrierCase2X2XV4_arg_regular line 227
  32. theorem OAI.InternalCatalan.barrierCase2X2XV4_weight_eq line 232
  33. theorem OAI.InternalCatalan.barrierCase2X2XV4_error line 237
  34. theorem OAI.InternalCatalan.barrierCase2X2XV4_approx_upper line 252
  35. theorem OAI.InternalCatalan.barrierCase2X2XV4_log_upper line 259
  36. def OAI.InternalCatalan.barrierCase2X2XV5LogArg line 270
  37. theorem OAI.InternalCatalan.barrierCase2X2XV5_arg_eq line 273
  38. theorem OAI.InternalCatalan.barrierCase2X2XV5_arg_regular line 279
  39. theorem OAI.InternalCatalan.barrierCase2X2XV5_weight_eq line 284
  40. theorem OAI.InternalCatalan.barrierCase2X2XV5_error line 289
  41. theorem OAI.InternalCatalan.barrierCase2X2XV5_approx_upper line 304
  42. theorem OAI.InternalCatalan.barrierCase2X2XV5_log_upper line 311
  43. def OAI.InternalCatalan.barrierCase2X2XV7LogArg line 322
  44. theorem OAI.InternalCatalan.barrierCase2X2XV7_arg_eq line 325
  45. theorem OAI.InternalCatalan.barrierCase2X2XV7_arg_regular line 331
  46. theorem OAI.InternalCatalan.barrierCase2X2XV7_weight_eq line 336
  47. theorem OAI.InternalCatalan.barrierCase2X2XV7_error line 341
  48. theorem OAI.InternalCatalan.barrierCase2X2XV7_approx_upper line 356
  49. theorem OAI.InternalCatalan.barrierCase2X2XV7_log_upper line 363
  50. def OAI.InternalCatalan.barrierCase2X2XV9LogArg line 374
  51. theorem OAI.InternalCatalan.barrierCase2X2XV9_arg_eq line 377
  52. theorem OAI.InternalCatalan.barrierCase2X2XV9_arg_regular line 383
  53. theorem OAI.InternalCatalan.barrierCase2X2XV9_weight_eq line 388
  54. theorem OAI.InternalCatalan.barrierCase2X2XV9_error line 393
  55. theorem OAI.InternalCatalan.barrierCase2X2XV9_approx_upper line 408
  56. theorem OAI.InternalCatalan.barrierCase2X2XV9_log_upper line 415
  57. def OAI.InternalCatalan.barrierCase2X2XV11LogArg line 426
  58. theorem OAI.InternalCatalan.barrierCase2X2XV11_arg_eq line 429
  59. theorem OAI.InternalCatalan.barrierCase2X2XV11_arg_regular line 435
  60. theorem OAI.InternalCatalan.barrierCase2X2XV11_weight_eq line 440
  61. theorem OAI.InternalCatalan.barrierCase2X2XV11_error line 445
  62. theorem OAI.InternalCatalan.barrierCase2X2XV11_approx_upper line 460
  63. theorem OAI.InternalCatalan.barrierCase2X2XV11_log_upper line 467
  64. theorem OAI.InternalCatalan.barrierCase2X2_XP_tail_upper line 480
  65. theorem OAI.InternalCatalan.barrierCase2X2_XV_tail_upper line 502
  66. theorem OAI.InternalCatalan.barrierCase2X2_approx_upper line 527
  67. theorem OAI.InternalCatalan.barrierCase2X2_lt line 535