OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoLogApprox.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.Case2PointData.X0_normalizations line 14
  2. theorem OAI.InternalCatalan.Case2PointData.X1_normalizations line 20
  3. theorem OAI.InternalCatalan.Case2PointData.X2_normalizations line 26
  4. theorem OAI.InternalCatalan.Case2PointData.X3_normalizations line 32
  5. theorem OAI.InternalCatalan.Case2PointData.X4_normalizations line 38
  6. theorem OAI.InternalCatalan.Case2PointData.X5_normalizations line 44
  7. theorem OAI.InternalCatalan.Case2PointData.X6_normalizations line 50
  8. theorem OAI.InternalCatalan.Case2PointData.X7_normalizations line 56
  9. theorem OAI.InternalCatalan.Case2PointData.X8_normalizations line 62
  10. theorem OAI.InternalCatalan.Case2PointData.X9_normalizations line 68
  11. theorem OAI.InternalCatalan.Case2PointData.X10_normalizations line 74
  12. theorem OAI.InternalCatalan.Case2PointData.X11_normalizations line 80
  13. theorem OAI.InternalCatalan.Case2PointData.X12_normalizations line 86
  14. theorem OAI.InternalCatalan.Case2PointData.X13_normalizations line 92
  15. theorem OAI.InternalCatalan.Case2PointData.X14_normalizations line 98
  16. theorem OAI.InternalCatalan.Case2PointData.X15_normalizations line 104
  17. theorem OAI.InternalCatalan.Case2PointData.X16_normalizations line 110
  18. theorem OAI.InternalCatalan.Case2PointData.X17_normalizations line 116
  19. theorem OAI.InternalCatalan.Case2PointData.X18_normalizations line 122
  20. theorem OAI.InternalCatalan.Case2PointData.Y0_normalizations line 128
  21. theorem OAI.InternalCatalan.Case2PointData.Y1_normalizations line 133
  22. theorem OAI.InternalCatalan.Case2PointData.Y2_normalizations line 138
  23. theorem OAI.InternalCatalan.Case2PointData.Y3_normalizations line 143
  24. theorem OAI.InternalCatalan.Case2PointData.Y4_normalizations line 148
  25. theorem OAI.InternalCatalan.Case2PointData.Y5_normalizations line 153
  26. theorem OAI.InternalCatalan.Case2PointData.Y6_normalizations line 158
  27. theorem OAI.InternalCatalan.Case2PointData.Y7_normalizations line 163
  28. theorem OAI.InternalCatalan.Case2PointData.Y8_normalizations line 168
  29. theorem OAI.InternalCatalan.Case2PointData.Y9_normalizations line 173
  30. theorem OAI.InternalCatalan.Case2PointData.Y10_normalizations line 178
  31. theorem OAI.InternalCatalan.Case2PointData.Y11_normalizations line 183
  32. theorem OAI.InternalCatalan.Case2PointData.Y12_normalizations line 188
  33. theorem OAI.InternalCatalan.Case2PointData.Y13_normalizations line 193
  34. theorem OAI.InternalCatalan.Case2PointData.Y14_normalizations line 198
  35. theorem OAI.InternalCatalan.Case2PointData.Y15_normalizations line 203
  36. theorem OAI.InternalCatalan.Case2PointData.Y16_normalizations line 208
  37. theorem OAI.InternalCatalan.Case2PointData.Y17_normalizations line 213
  38. def OAI.InternalCatalan.barrierCase2XApproxRat line 220
  39. def OAI.InternalCatalan.barrierCase2YApproxRat line 225
  40. theorem OAI.InternalCatalan.barrierCase2X_realLog_approx_error line 229
  41. theorem OAI.InternalCatalan.barrierCase2Y_realLog_approx_error line 248