OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoLogsX8Group0.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2X8XP0LogArg line 11
  2. theorem OAI.InternalCatalan.barrierCase2X8XP0_arg_eq line 14
  3. theorem OAI.InternalCatalan.barrierCase2X8XP0_arg_regular line 20
  4. theorem OAI.InternalCatalan.barrierCase2X8XP0_weight_eq line 25
  5. theorem OAI.InternalCatalan.barrierCase2X8XP0_error line 30
  6. theorem OAI.InternalCatalan.barrierCase2X8XP0_approx_upper line 45
  7. theorem OAI.InternalCatalan.barrierCase2X8XP0_log_upper line 52
  8. def OAI.InternalCatalan.barrierCase2X8XP1LogArg line 63
  9. theorem OAI.InternalCatalan.barrierCase2X8XP1_arg_eq line 66
  10. theorem OAI.InternalCatalan.barrierCase2X8XP1_arg_regular line 72
  11. theorem OAI.InternalCatalan.barrierCase2X8XP1_weight_eq line 77
  12. theorem OAI.InternalCatalan.barrierCase2X8XP1_error line 82
  13. theorem OAI.InternalCatalan.barrierCase2X8XP1_approx_upper line 97
  14. theorem OAI.InternalCatalan.barrierCase2X8XP1_log_upper line 104
  15. def OAI.InternalCatalan.barrierCase2X8XP2LogArg line 115
  16. theorem OAI.InternalCatalan.barrierCase2X8XP2_arg_eq line 118
  17. theorem OAI.InternalCatalan.barrierCase2X8XP2_arg_regular line 124
  18. theorem OAI.InternalCatalan.barrierCase2X8XP2_weight_eq line 129
  19. theorem OAI.InternalCatalan.barrierCase2X8XP2_error line 134
  20. theorem OAI.InternalCatalan.barrierCase2X8XP2_approx_upper line 149
  21. theorem OAI.InternalCatalan.barrierCase2X8XP2_log_upper line 156
  22. def OAI.InternalCatalan.barrierCase2X8XP4LogArg line 167
  23. theorem OAI.InternalCatalan.barrierCase2X8XP4_arg_eq line 170
  24. theorem OAI.InternalCatalan.barrierCase2X8XP4_arg_regular line 176
  25. theorem OAI.InternalCatalan.barrierCase2X8XP4_weight_eq line 181
  26. theorem OAI.InternalCatalan.barrierCase2X8XP4_error line 186
  27. theorem OAI.InternalCatalan.barrierCase2X8XP4_approx_upper line 201
  28. theorem OAI.InternalCatalan.barrierCase2X8XP4_log_upper line 208
  29. def OAI.InternalCatalan.barrierCase2X8XP6LogArg line 219
  30. theorem OAI.InternalCatalan.barrierCase2X8XP6_arg_eq line 222
  31. theorem OAI.InternalCatalan.barrierCase2X8XP6_arg_regular line 228
  32. theorem OAI.InternalCatalan.barrierCase2X8XP6_weight_eq line 233
  33. theorem OAI.InternalCatalan.barrierCase2X8XP6_error line 238
  34. theorem OAI.InternalCatalan.barrierCase2X8XP6_approx_upper line 253
  35. theorem OAI.InternalCatalan.barrierCase2X8XP6_log_upper line 260
  36. def OAI.InternalCatalan.barrierCase2X8XP8LogArg line 271
  37. theorem OAI.InternalCatalan.barrierCase2X8XP8_arg_eq line 274
  38. theorem OAI.InternalCatalan.barrierCase2X8XP8_arg_regular line 280
  39. theorem OAI.InternalCatalan.barrierCase2X8XP8_weight_eq line 285
  40. theorem OAI.InternalCatalan.barrierCase2X8XP8_error line 290
  41. theorem OAI.InternalCatalan.barrierCase2X8XP8_approx_upper line 305
  42. theorem OAI.InternalCatalan.barrierCase2X8XP8_log_upper line 312