OAI/NumberTheory/Catalan/Estimates/FixedTypedChebyshevT39To41.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.fixedTyped_chebyshevT_link line 13
  2. theorem OAI.InternalCatalan.fixedTyped_chebyshevU_link line 19
  3. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_0 line 35
  4. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_1 line 39
  5. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_2 line 43
  6. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_3 line 70
  7. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_4 line 97
  8. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_5 line 124
  9. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_6 line 151
  10. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_7 line 178
  11. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_8 line 205
  12. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_9 line 232
  13. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_10 line 259
  14. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_11 line 296
  15. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_12 line 323
  16. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_13 line 350
  17. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_14 line 377
  18. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_15 line 404
  19. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_16 line 431
  20. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_17 line 458
  21. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_18 line 495
  22. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_19 line 522
  23. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_20 line 549
  24. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_21 line 576
  25. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_22 line 603
  26. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_23 line 630
  27. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_24 line 667
  28. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_25 line 693
  29. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_26 line 719
  30. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_27 line 745
  31. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_28 line 771
  32. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_24 line 807
  33. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_25 line 833
  34. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_26 line 859
  35. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_27 line 885
  36. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_28 line 911
  37. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_29 line 947
  38. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_30 line 973
  39. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_31 line 999
  40. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_32 line 1025
  41. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_33 line 1061
  42. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_34 line 1087
  43. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_35 line 1113
  44. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_36 line 1149
  45. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_37 line 1175
  46. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_38 line 1201
  47. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_39 line 1237
  48. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_40 line 1263
  49. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_41 line 1289