OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointY0.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2Y0YV0LogArg line 9
  2. theorem OAI.InternalCatalan.barrierCase2Y0YV0_arg_eq line 12
  3. theorem OAI.InternalCatalan.barrierCase2Y0YV0_arg_regular line 18
  4. theorem OAI.InternalCatalan.barrierCase2Y0YV0_weight_eq line 23
  5. theorem OAI.InternalCatalan.barrierCase2Y0YV0_error line 28
  6. theorem OAI.InternalCatalan.barrierCase2Y0YV0_approx_upper line 43
  7. theorem OAI.InternalCatalan.barrierCase2Y0YV0_log_upper line 50
  8. def OAI.InternalCatalan.barrierCase2Y0YV1LogArg line 66
  9. theorem OAI.InternalCatalan.barrierCase2Y0YV1_arg_eq line 69
  10. theorem OAI.InternalCatalan.barrierCase2Y0YV1_arg_regular line 75
  11. theorem OAI.InternalCatalan.barrierCase2Y0YV1_weight_eq line 80
  12. theorem OAI.InternalCatalan.barrierCase2Y0YV1_error line 85
  13. theorem OAI.InternalCatalan.barrierCase2Y0YV1_approx_upper line 100
  14. theorem OAI.InternalCatalan.barrierCase2Y0YV1_log_upper line 107
  15. def OAI.InternalCatalan.barrierCase2Y0YV2LogArg line 118
  16. theorem OAI.InternalCatalan.barrierCase2Y0YV2_arg_eq line 121
  17. theorem OAI.InternalCatalan.barrierCase2Y0YV2_arg_regular line 127
  18. theorem OAI.InternalCatalan.barrierCase2Y0YV2_weight_eq line 132
  19. theorem OAI.InternalCatalan.barrierCase2Y0YV2_error line 137
  20. theorem OAI.InternalCatalan.barrierCase2Y0YV2_approx_upper line 152
  21. theorem OAI.InternalCatalan.barrierCase2Y0YV2_log_upper line 159
  22. def OAI.InternalCatalan.barrierCase2Y0YV3LogArg line 170
  23. theorem OAI.InternalCatalan.barrierCase2Y0YV3_arg_eq line 173
  24. theorem OAI.InternalCatalan.barrierCase2Y0YV3_arg_regular line 179
  25. theorem OAI.InternalCatalan.barrierCase2Y0YV3_weight_eq line 184
  26. theorem OAI.InternalCatalan.barrierCase2Y0YV3_error line 189
  27. theorem OAI.InternalCatalan.barrierCase2Y0YV3_approx_upper line 204
  28. theorem OAI.InternalCatalan.barrierCase2Y0YV3_log_upper line 211
  29. def OAI.InternalCatalan.barrierCase2Y0YV4LogArg line 222
  30. theorem OAI.InternalCatalan.barrierCase2Y0YV4_arg_eq line 225
  31. theorem OAI.InternalCatalan.barrierCase2Y0YV4_arg_regular line 231
  32. theorem OAI.InternalCatalan.barrierCase2Y0YV4_weight_eq line 236
  33. theorem OAI.InternalCatalan.barrierCase2Y0YV4_error line 241
  34. theorem OAI.InternalCatalan.barrierCase2Y0YV4_approx_upper line 256
  35. theorem OAI.InternalCatalan.barrierCase2Y0YV4_log_upper line 263
  36. def OAI.InternalCatalan.barrierCase2Y0YV5LogArg line 274
  37. theorem OAI.InternalCatalan.barrierCase2Y0YV5_arg_eq line 277
  38. theorem OAI.InternalCatalan.barrierCase2Y0YV5_arg_regular line 283
  39. theorem OAI.InternalCatalan.barrierCase2Y0YV5_weight_eq line 288
  40. theorem OAI.InternalCatalan.barrierCase2Y0YV5_error line 293
  41. theorem OAI.InternalCatalan.barrierCase2Y0YV5_approx_upper line 308
  42. theorem OAI.InternalCatalan.barrierCase2Y0YV5_log_upper line 315
  43. def OAI.InternalCatalan.barrierCase2Y0YV7LogArg line 326
  44. theorem OAI.InternalCatalan.barrierCase2Y0YV7_arg_eq line 329
  45. theorem OAI.InternalCatalan.barrierCase2Y0YV7_arg_regular line 335
  46. theorem OAI.InternalCatalan.barrierCase2Y0YV7_weight_eq line 340
  47. theorem OAI.InternalCatalan.barrierCase2Y0YV7_error line 345
  48. theorem OAI.InternalCatalan.barrierCase2Y0YV7_approx_upper line 360
  49. theorem OAI.InternalCatalan.barrierCase2Y0YV7_log_upper line 367
  50. def OAI.InternalCatalan.barrierCase2Y0YV9LogArg line 383
  51. theorem OAI.InternalCatalan.barrierCase2Y0YV9_arg_eq line 386
  52. theorem OAI.InternalCatalan.barrierCase2Y0YV9_arg_regular line 392
  53. theorem OAI.InternalCatalan.barrierCase2Y0YV9_weight_eq line 397
  54. theorem OAI.InternalCatalan.barrierCase2Y0YV9_error line 402
  55. theorem OAI.InternalCatalan.barrierCase2Y0YV9_approx_upper line 417
  56. theorem OAI.InternalCatalan.barrierCase2Y0YV9_log_upper line 424
  57. def OAI.InternalCatalan.barrierCase2Y0YV11LogArg line 435
  58. theorem OAI.InternalCatalan.barrierCase2Y0YV11_arg_eq line 438
  59. theorem OAI.InternalCatalan.barrierCase2Y0YV11_arg_regular line 444
  60. theorem OAI.InternalCatalan.barrierCase2Y0YV11_weight_eq line 449
  61. theorem OAI.InternalCatalan.barrierCase2Y0YV11_error line 454
  62. theorem OAI.InternalCatalan.barrierCase2Y0YV11_approx_upper line 469
  63. theorem OAI.InternalCatalan.barrierCase2Y0YV11_log_upper line 476
  64. theorem OAI.InternalCatalan.barrierCase2Y0_YV_tail_upper line 493
  65. theorem OAI.InternalCatalan.barrierCase2Y0_approx_upper line 518
  66. theorem OAI.InternalCatalan.barrierCase2Y0_lt line 526