OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoLogsX5Group0.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2X5XP0LogArg line 10
  2. theorem OAI.InternalCatalan.barrierCase2X5XP0_arg_eq line 13
  3. theorem OAI.InternalCatalan.barrierCase2X5XP0_arg_regular line 19
  4. theorem OAI.InternalCatalan.barrierCase2X5XP0_weight_eq line 24
  5. theorem OAI.InternalCatalan.barrierCase2X5XP0_error line 29
  6. theorem OAI.InternalCatalan.barrierCase2X5XP0_approx_upper line 44
  7. theorem OAI.InternalCatalan.barrierCase2X5XP0_log_upper line 51
  8. def OAI.InternalCatalan.barrierCase2X5XP1LogArg line 62
  9. theorem OAI.InternalCatalan.barrierCase2X5XP1_arg_eq line 65
  10. theorem OAI.InternalCatalan.barrierCase2X5XP1_arg_regular line 71
  11. theorem OAI.InternalCatalan.barrierCase2X5XP1_weight_eq line 76
  12. theorem OAI.InternalCatalan.barrierCase2X5XP1_error line 81
  13. theorem OAI.InternalCatalan.barrierCase2X5XP1_approx_upper line 96
  14. theorem OAI.InternalCatalan.barrierCase2X5XP1_log_upper line 103
  15. def OAI.InternalCatalan.barrierCase2X5XP2LogArg line 114
  16. theorem OAI.InternalCatalan.barrierCase2X5XP2_arg_eq line 117
  17. theorem OAI.InternalCatalan.barrierCase2X5XP2_arg_regular line 123
  18. theorem OAI.InternalCatalan.barrierCase2X5XP2_weight_eq line 128
  19. theorem OAI.InternalCatalan.barrierCase2X5XP2_error line 133
  20. theorem OAI.InternalCatalan.barrierCase2X5XP2_approx_upper line 148
  21. theorem OAI.InternalCatalan.barrierCase2X5XP2_log_upper line 155
  22. def OAI.InternalCatalan.barrierCase2X5XP4LogArg line 166
  23. theorem OAI.InternalCatalan.barrierCase2X5XP4_arg_eq line 169
  24. theorem OAI.InternalCatalan.barrierCase2X5XP4_arg_regular line 175
  25. theorem OAI.InternalCatalan.barrierCase2X5XP4_weight_eq line 180
  26. theorem OAI.InternalCatalan.barrierCase2X5XP4_error line 185
  27. theorem OAI.InternalCatalan.barrierCase2X5XP4_approx_upper line 200
  28. theorem OAI.InternalCatalan.barrierCase2X5XP4_log_upper line 207
  29. def OAI.InternalCatalan.barrierCase2X5XP6LogArg line 218
  30. theorem OAI.InternalCatalan.barrierCase2X5XP6_arg_eq line 221
  31. theorem OAI.InternalCatalan.barrierCase2X5XP6_arg_regular line 227
  32. theorem OAI.InternalCatalan.barrierCase2X5XP6_weight_eq line 232
  33. theorem OAI.InternalCatalan.barrierCase2X5XP6_error line 237
  34. theorem OAI.InternalCatalan.barrierCase2X5XP6_approx_upper line 252
  35. theorem OAI.InternalCatalan.barrierCase2X5XP6_log_upper line 259
  36. def OAI.InternalCatalan.barrierCase2X5XP8LogArg line 270
  37. theorem OAI.InternalCatalan.barrierCase2X5XP8_arg_eq line 273
  38. theorem OAI.InternalCatalan.barrierCase2X5XP8_arg_regular line 279
  39. theorem OAI.InternalCatalan.barrierCase2X5XP8_weight_eq line 284
  40. theorem OAI.InternalCatalan.barrierCase2X5XP8_error line 289
  41. theorem OAI.InternalCatalan.barrierCase2X5XP8_approx_upper line 304
  42. theorem OAI.InternalCatalan.barrierCase2X5XP8_log_upper line 311