OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOnePointLogInputs.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.Case1PointData.FixedLogNormalization line 9
  2. def OAI.InternalCatalan.Case1PointData.X0 line 13
  3. def OAI.InternalCatalan.Case1PointData.X0PrintedUpper line 15
  4. theorem OAI.InternalCatalan.Case1PointData.X0_normalizations line 17
  5. def OAI.InternalCatalan.Case1PointData.X1 line 23
  6. def OAI.InternalCatalan.Case1PointData.X1PrintedUpper line 25
  7. theorem OAI.InternalCatalan.Case1PointData.X1_normalizations line 27
  8. def OAI.InternalCatalan.Case1PointData.X2 line 33
  9. def OAI.InternalCatalan.Case1PointData.X2PrintedUpper line 35
  10. theorem OAI.InternalCatalan.Case1PointData.X2_normalizations line 37
  11. def OAI.InternalCatalan.Case1PointData.X3 line 43
  12. def OAI.InternalCatalan.Case1PointData.X3PrintedUpper line 45
  13. theorem OAI.InternalCatalan.Case1PointData.X3_normalizations line 47
  14. def OAI.InternalCatalan.Case1PointData.X4 line 53
  15. def OAI.InternalCatalan.Case1PointData.X4PrintedUpper line 55
  16. theorem OAI.InternalCatalan.Case1PointData.X4_normalizations line 57
  17. def OAI.InternalCatalan.Case1PointData.X5 line 63
  18. def OAI.InternalCatalan.Case1PointData.X5PrintedUpper line 65
  19. theorem OAI.InternalCatalan.Case1PointData.X5_normalizations line 67
  20. def OAI.InternalCatalan.Case1PointData.X6 line 73
  21. def OAI.InternalCatalan.Case1PointData.X6PrintedUpper line 75
  22. theorem OAI.InternalCatalan.Case1PointData.X6_normalizations line 77
  23. def OAI.InternalCatalan.Case1PointData.X7 line 83
  24. def OAI.InternalCatalan.Case1PointData.X7PrintedUpper line 85
  25. theorem OAI.InternalCatalan.Case1PointData.X7_normalizations line 87
  26. def OAI.InternalCatalan.Case1PointData.Y0 line 93
  27. def OAI.InternalCatalan.Case1PointData.Y0PrintedUpper line 95
  28. theorem OAI.InternalCatalan.Case1PointData.Y0_normalizations line 97
  29. def OAI.InternalCatalan.Case1PointData.Y1 line 102
  30. def OAI.InternalCatalan.Case1PointData.Y1PrintedUpper line 104
  31. theorem OAI.InternalCatalan.Case1PointData.Y1_normalizations line 106
  32. def OAI.InternalCatalan.Case1PointData.Y2 line 111
  33. def OAI.InternalCatalan.Case1PointData.Y2PrintedUpper line 113
  34. theorem OAI.InternalCatalan.Case1PointData.Y2_normalizations line 115
  35. def OAI.InternalCatalan.Case1PointData.Y3 line 120
  36. def OAI.InternalCatalan.Case1PointData.Y3PrintedUpper line 122
  37. theorem OAI.InternalCatalan.Case1PointData.Y3_normalizations line 124
  38. def OAI.InternalCatalan.Case1PointData.Y4 line 129
  39. def OAI.InternalCatalan.Case1PointData.Y4PrintedUpper line 131
  40. theorem OAI.InternalCatalan.Case1PointData.Y4_normalizations line 133