OAI/NumberTheory/Catalan/Estimates/FixedTypedChebyshevTData.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedChebyshevTData_0 line 10
  2. def OAI.InternalCatalan.fixedChebyshevTData_1 line 13
  3. def OAI.InternalCatalan.fixedChebyshevTData_2 line 16
  4. def OAI.InternalCatalan.fixedChebyshevTData_3 line 20
  5. def OAI.InternalCatalan.fixedChebyshevTData_4 line 24
  6. def OAI.InternalCatalan.fixedChebyshevTData_5 line 29
  7. def OAI.InternalCatalan.fixedChebyshevTData_6 line 34
  8. def OAI.InternalCatalan.fixedChebyshevTData_7 line 40
  9. def OAI.InternalCatalan.fixedChebyshevTData_8 line 46
  10. def OAI.InternalCatalan.fixedChebyshevTData_9 line 53
  11. def OAI.InternalCatalan.fixedChebyshevTData_10 line 60
  12. def OAI.InternalCatalan.fixedChebyshevTData_11 line 68
  13. def OAI.InternalCatalan.fixedChebyshevTData_12 line 76
  14. def OAI.InternalCatalan.fixedChebyshevTData_13 line 85
  15. def OAI.InternalCatalan.fixedChebyshevTData_14 line 94
  16. def OAI.InternalCatalan.fixedChebyshevTData_15 line 104
  17. def OAI.InternalCatalan.fixedChebyshevTData_16 line 114
  18. def OAI.InternalCatalan.fixedChebyshevTData_17 line 125
  19. def OAI.InternalCatalan.fixedChebyshevTData_18 line 136
  20. def OAI.InternalCatalan.fixedChebyshevTData_19 line 148
  21. def OAI.InternalCatalan.fixedChebyshevTData_20 line 160
  22. def OAI.InternalCatalan.fixedChebyshevTData_21 line 173
  23. def OAI.InternalCatalan.fixedChebyshevTData_22 line 186
  24. def OAI.InternalCatalan.fixedChebyshevTData_23 line 200
  25. def OAI.InternalCatalan.fixedChebyshevTData_24 line 214
  26. def OAI.InternalCatalan.fixedChebyshevTData_25 line 229
  27. def OAI.InternalCatalan.fixedChebyshevTData_26 line 244
  28. def OAI.InternalCatalan.fixedChebyshevTData_27 line 260
  29. def OAI.InternalCatalan.fixedChebyshevTData_28 line 276
  30. def OAI.InternalCatalan.fixedChebyshevTData_29 line 293
  31. def OAI.InternalCatalan.fixedChebyshevTData_30 line 310
  32. def OAI.InternalCatalan.fixedChebyshevTData_31 line 328
  33. def OAI.InternalCatalan.fixedChebyshevTData_32 line 346
  34. def OAI.InternalCatalan.fixedChebyshevTData_33 line 365
  35. def OAI.InternalCatalan.fixedChebyshevTData_34 line 384
  36. def OAI.InternalCatalan.fixedChebyshevTData_35 line 404
  37. def OAI.InternalCatalan.fixedChebyshevTData_36 line 424
  38. def OAI.InternalCatalan.fixedChebyshevTData_37 line 445
  39. def OAI.InternalCatalan.fixedChebyshevTData_38 line 466
  40. def OAI.InternalCatalan.fixedChebyshevTData_39 line 488
  41. def OAI.InternalCatalan.fixedChebyshevTData_40 line 510
  42. def OAI.InternalCatalan.fixedChebyshevTData_41 line 533
  43. def OAI.InternalCatalan.fixedChebyshevTData_42 line 556
  44. def OAI.InternalCatalan.fixedChebyshevTData_43 line 580
  45. def OAI.InternalCatalan.fixedChebyshevTData_44 line 604