OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedT0To7.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_29 line 12
  2. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_30 line 38
  3. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_31 line 64
  4. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_32 line 90
  5. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_33 line 126
  6. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_34 line 152
  7. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_35 line 178
  8. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_36 line 214
  9. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_37 line 240
  10. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_38 line 266
  11. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_39 line 302
  12. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_40 line 328
  13. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_41 line 354
  14. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_42 line 390
  15. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_43 line 416
  16. theorem OAI.InternalCatalan.fixed_chebyshevT_typed_44 line 442
  17. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_42 line 478
  18. theorem OAI.InternalCatalan.fixed_chebyshevU_typed_43 line 504
  19. def OAI.InternalCatalan.fixedReversedTData_0 line 541
  20. def OAI.InternalCatalan.fixedReversedTCoeff_0 line 544
  21. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_0 line 547
  22. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_0 line 551
  23. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_0 line 555
  24. def OAI.InternalCatalan.fixedReversedTData_1 line 559
  25. def OAI.InternalCatalan.fixedReversedTCoeff_1 line 562
  26. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_1 line 565
  27. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_1 line 569
  28. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_1 line 573
  29. def OAI.InternalCatalan.fixedReversedTData_2 line 577
  30. def OAI.InternalCatalan.fixedReversedTCoeff_2 line 581
  31. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_2 line 585
  32. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_2 line 590
  33. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_2 line 594
  34. def OAI.InternalCatalan.fixedReversedTData_3 line 598
  35. def OAI.InternalCatalan.fixedReversedTCoeff_3 line 602
  36. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_3 line 606
  37. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_3 line 611
  38. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_3 line 615
  39. def OAI.InternalCatalan.fixedReversedTData_4 line 619
  40. def OAI.InternalCatalan.fixedReversedTCoeff_4 line 624
  41. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_4 line 629
  42. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_4 line 635
  43. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_4 line 639
  44. def OAI.InternalCatalan.fixedReversedTData_5 line 643
  45. def OAI.InternalCatalan.fixedReversedTCoeff_5 line 648
  46. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_5 line 653
  47. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_5 line 659
  48. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_5 line 663
  49. def OAI.InternalCatalan.fixedReversedTData_6 line 667
  50. def OAI.InternalCatalan.fixedReversedTCoeff_6 line 673
  51. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_6 line 679
  52. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_6 line 686
  53. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_6 line 690
  54. def OAI.InternalCatalan.fixedReversedTData_7 line 694
  55. def OAI.InternalCatalan.fixedReversedTCoeff_7 line 700
  56. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_7 line 706
  57. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_7 line 713
  58. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_7 line 717