OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoPointY5.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2Y5YV0LogArg line 9
  2. theorem OAI.InternalCatalan.barrierCase2Y5YV0_arg_eq line 12
  3. theorem OAI.InternalCatalan.barrierCase2Y5YV0_arg_regular line 18
  4. theorem OAI.InternalCatalan.barrierCase2Y5YV0_weight_eq line 23
  5. theorem OAI.InternalCatalan.barrierCase2Y5YV0_error line 28
  6. theorem OAI.InternalCatalan.barrierCase2Y5YV0_approx_upper line 43
  7. theorem OAI.InternalCatalan.barrierCase2Y5YV0_log_upper line 50
  8. def OAI.InternalCatalan.barrierCase2Y5YV1LogArg line 61
  9. theorem OAI.InternalCatalan.barrierCase2Y5YV1_arg_eq line 64
  10. theorem OAI.InternalCatalan.barrierCase2Y5YV1_arg_regular line 70
  11. theorem OAI.InternalCatalan.barrierCase2Y5YV1_weight_eq line 75
  12. theorem OAI.InternalCatalan.barrierCase2Y5YV1_error line 80
  13. theorem OAI.InternalCatalan.barrierCase2Y5YV1_approx_upper line 95
  14. theorem OAI.InternalCatalan.barrierCase2Y5YV1_log_upper line 102
  15. def OAI.InternalCatalan.barrierCase2Y5YV2LogArg line 113
  16. theorem OAI.InternalCatalan.barrierCase2Y5YV2_arg_eq line 116
  17. theorem OAI.InternalCatalan.barrierCase2Y5YV2_arg_regular line 122
  18. theorem OAI.InternalCatalan.barrierCase2Y5YV2_weight_eq line 127
  19. theorem OAI.InternalCatalan.barrierCase2Y5YV2_error line 132
  20. theorem OAI.InternalCatalan.barrierCase2Y5YV2_approx_upper line 147
  21. theorem OAI.InternalCatalan.barrierCase2Y5YV2_log_upper line 154
  22. def OAI.InternalCatalan.barrierCase2Y5YV3LogArg line 165
  23. theorem OAI.InternalCatalan.barrierCase2Y5YV3_arg_eq line 168
  24. theorem OAI.InternalCatalan.barrierCase2Y5YV3_arg_regular line 174
  25. theorem OAI.InternalCatalan.barrierCase2Y5YV3_weight_eq line 179
  26. theorem OAI.InternalCatalan.barrierCase2Y5YV3_error line 184
  27. theorem OAI.InternalCatalan.barrierCase2Y5YV3_approx_upper line 199
  28. theorem OAI.InternalCatalan.barrierCase2Y5YV3_log_upper line 206
  29. def OAI.InternalCatalan.barrierCase2Y5YV4LogArg line 217
  30. theorem OAI.InternalCatalan.barrierCase2Y5YV4_arg_eq line 220
  31. theorem OAI.InternalCatalan.barrierCase2Y5YV4_arg_regular line 226
  32. theorem OAI.InternalCatalan.barrierCase2Y5YV4_weight_eq line 231
  33. theorem OAI.InternalCatalan.barrierCase2Y5YV4_error line 236
  34. theorem OAI.InternalCatalan.barrierCase2Y5YV4_approx_upper line 251
  35. theorem OAI.InternalCatalan.barrierCase2Y5YV4_log_upper line 258
  36. def OAI.InternalCatalan.barrierCase2Y5YV5LogArg line 269
  37. theorem OAI.InternalCatalan.barrierCase2Y5YV5_arg_eq line 272
  38. theorem OAI.InternalCatalan.barrierCase2Y5YV5_arg_regular line 278
  39. theorem OAI.InternalCatalan.barrierCase2Y5YV5_weight_eq line 283
  40. theorem OAI.InternalCatalan.barrierCase2Y5YV5_error line 288
  41. theorem OAI.InternalCatalan.barrierCase2Y5YV5_approx_upper line 303
  42. theorem OAI.InternalCatalan.barrierCase2Y5YV5_log_upper line 310
  43. def OAI.InternalCatalan.barrierCase2Y5YV7LogArg line 326
  44. theorem OAI.InternalCatalan.barrierCase2Y5YV7_arg_eq line 329
  45. theorem OAI.InternalCatalan.barrierCase2Y5YV7_arg_regular line 335
  46. theorem OAI.InternalCatalan.barrierCase2Y5YV7_weight_eq line 340
  47. theorem OAI.InternalCatalan.barrierCase2Y5YV7_error line 345
  48. theorem OAI.InternalCatalan.barrierCase2Y5YV7_approx_upper line 360
  49. theorem OAI.InternalCatalan.barrierCase2Y5YV7_log_upper line 367
  50. def OAI.InternalCatalan.barrierCase2Y5YV9LogArg line 378
  51. theorem OAI.InternalCatalan.barrierCase2Y5YV9_arg_eq line 381
  52. theorem OAI.InternalCatalan.barrierCase2Y5YV9_arg_regular line 387
  53. theorem OAI.InternalCatalan.barrierCase2Y5YV9_weight_eq line 392
  54. theorem OAI.InternalCatalan.barrierCase2Y5YV9_error line 397
  55. theorem OAI.InternalCatalan.barrierCase2Y5YV9_approx_upper line 412
  56. theorem OAI.InternalCatalan.barrierCase2Y5YV9_log_upper line 419
  57. def OAI.InternalCatalan.barrierCase2Y5YV11LogArg line 430
  58. theorem OAI.InternalCatalan.barrierCase2Y5YV11_arg_eq line 433
  59. theorem OAI.InternalCatalan.barrierCase2Y5YV11_arg_regular line 439
  60. theorem OAI.InternalCatalan.barrierCase2Y5YV11_weight_eq line 444
  61. theorem OAI.InternalCatalan.barrierCase2Y5YV11_error line 449
  62. theorem OAI.InternalCatalan.barrierCase2Y5YV11_approx_upper line 464
  63. theorem OAI.InternalCatalan.barrierCase2Y5YV11_log_upper line 471
  64. theorem OAI.InternalCatalan.barrierCase2Y5_YV_tail_upper line 488
  65. theorem OAI.InternalCatalan.barrierCase2Y5_approx_upper line 513
  66. theorem OAI.InternalCatalan.barrierCase2Y5_lt line 521