OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoLogsSixControl.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2X14XP2LogArg line 10
  2. theorem OAI.InternalCatalan.barrierCase2X14XP2_arg_eq line 13
  3. theorem OAI.InternalCatalan.barrierCase2X14XP2_arg_regular line 19
  4. theorem OAI.InternalCatalan.barrierCase2X14XP2_weight_eq line 24
  5. theorem OAI.InternalCatalan.barrierCase2X14XP2_error line 29
  6. theorem OAI.InternalCatalan.barrierCase2X14XP2_approx_upper line 44
  7. theorem OAI.InternalCatalan.barrierCase2X14XP2_log_upper line 51
  8. def OAI.InternalCatalan.barrierCase2X14XP4LogArg line 62
  9. theorem OAI.InternalCatalan.barrierCase2X14XP4_arg_eq line 65
  10. theorem OAI.InternalCatalan.barrierCase2X14XP4_arg_regular line 71
  11. theorem OAI.InternalCatalan.barrierCase2X14XP4_weight_eq line 76
  12. theorem OAI.InternalCatalan.barrierCase2X14XP4_error line 81
  13. theorem OAI.InternalCatalan.barrierCase2X14XP4_approx_upper line 96
  14. theorem OAI.InternalCatalan.barrierCase2X14XP4_log_upper line 103
  15. def OAI.InternalCatalan.barrierCase2X14XP6LogArg line 114
  16. theorem OAI.InternalCatalan.barrierCase2X14XP6_arg_eq line 117
  17. theorem OAI.InternalCatalan.barrierCase2X14XP6_arg_regular line 123
  18. theorem OAI.InternalCatalan.barrierCase2X14XP6_weight_eq line 128
  19. theorem OAI.InternalCatalan.barrierCase2X14XP6_error line 133
  20. theorem OAI.InternalCatalan.barrierCase2X14XP6_approx_upper line 148
  21. theorem OAI.InternalCatalan.barrierCase2X14XP6_log_upper line 155
  22. def OAI.InternalCatalan.barrierCase2X14XP8LogArg line 166
  23. theorem OAI.InternalCatalan.barrierCase2X14XP8_arg_eq line 169
  24. theorem OAI.InternalCatalan.barrierCase2X14XP8_arg_regular line 175
  25. theorem OAI.InternalCatalan.barrierCase2X14XP8_weight_eq line 180
  26. theorem OAI.InternalCatalan.barrierCase2X14XP8_error line 185
  27. theorem OAI.InternalCatalan.barrierCase2X14XP8_approx_upper line 200
  28. theorem OAI.InternalCatalan.barrierCase2X14XP8_log_upper line 207
  29. def OAI.InternalCatalan.barrierCase2X14XV5LogArg line 218
  30. theorem OAI.InternalCatalan.barrierCase2X14XV5_arg_eq line 221
  31. theorem OAI.InternalCatalan.barrierCase2X14XV5_arg_regular line 227
  32. theorem OAI.InternalCatalan.barrierCase2X14XV5_weight_eq line 232
  33. theorem OAI.InternalCatalan.barrierCase2X14XV5_error line 237
  34. theorem OAI.InternalCatalan.barrierCase2X14XV5_approx_upper line 252
  35. theorem OAI.InternalCatalan.barrierCase2X14XV5_log_upper line 259
  36. def OAI.InternalCatalan.barrierCase2X14XV7LogArg line 270
  37. theorem OAI.InternalCatalan.barrierCase2X14XV7_arg_eq line 273
  38. theorem OAI.InternalCatalan.barrierCase2X14XV7_arg_regular line 279
  39. theorem OAI.InternalCatalan.barrierCase2X14XV7_weight_eq line 284
  40. theorem OAI.InternalCatalan.barrierCase2X14XV7_error line 289
  41. theorem OAI.InternalCatalan.barrierCase2X14XV7_approx_upper line 304
  42. theorem OAI.InternalCatalan.barrierCase2X14XV7_log_upper line 311