OAI/NumberTheory/Catalan/Estimates/PalindromicStarParameters.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.palindromicRatW line 20
  2. def OAI.InternalCatalan.palindromicRatT line 23
  3. def OAI.InternalCatalan.palindromicRatF line 26
  4. def OAI.InternalCatalan.palindromicRatE line 29
  5. theorem OAI.InternalCatalan.palindromicRat_map_one_add_X_sq line 32
  6. theorem OAI.InternalCatalan.palindromicRat_map_one_sub_X_sq line 37
  7. theorem OAI.InternalCatalan.palindromic_one_add_X_sq_ne_zero line 42
  8. theorem OAI.InternalCatalan.palindromicRat_denominator_ne_zero line 50
  9. theorem OAI.InternalCatalan.palindromicRat_F_sq line 57
  10. theorem OAI.InternalCatalan.palindromic_prime_pred_twice_half line 63
  11. theorem OAI.InternalCatalan.palindromicRat_E_eq_F_pow line 68
  12. theorem OAI.InternalCatalan.palindromicRatW_transcendental line 83
  13. theorem OAI.InternalCatalan.palindromicRatW_ne_zero line 89
  14. theorem OAI.InternalCatalan.palindromicRatW_inv_transcendental line 96
  15. theorem OAI.InternalCatalan.palindromicRatW_inv_eval₂RingHom_injective line 101
  16. def OAI.InternalCatalan.palindromicRatStar line 107
  17. theorem OAI.InternalCatalan.palindromicRatStar_map_polynomial line 115
  18. theorem OAI.InternalCatalan.palindromicRatStar_W line 122
  19. theorem OAI.InternalCatalan.palindromicRatStar_scalar line 127
  20. theorem OAI.InternalCatalan.palindromicRatStar_injective line 141
  21. theorem OAI.InternalCatalan.palindromicRatT_ne_C line 155
  22. theorem OAI.InternalCatalan.palindromicRatT_transcendental line 173
  23. theorem OAI.InternalCatalan.palindromicRatT_aeval_injective line 200
  24. theorem OAI.InternalCatalan.palindromicRatT_eval₂RingHom_injective line 205
  25. theorem OAI.InternalCatalan.palindromicRatT_eval₂_eq_zero_iff line 212
  26. theorem OAI.InternalCatalan.palindromic_denominator_cleared_expansion line 234
  27. theorem OAI.InternalCatalan.palindromicRat_map_C line 243
  28. theorem OAI.InternalCatalan.palindromicRat_map_U line 249
  29. theorem OAI.InternalCatalan.palindromicRat_F_pow_expansion line 263
  30. theorem OAI.InternalCatalan.palindromicRat_expansion line 295
  31. theorem OAI.InternalCatalan.palindromicRat_W_ne_zero line 318
  32. theorem OAI.InternalCatalan.palindromicRat_two_pow line 322
  33. theorem OAI.InternalCatalan.palindromicRat_T_frobenius line 327
  34. theorem OAI.InternalCatalan.palindromicRat_F_frobenius line 335
  35. theorem OAI.InternalCatalan.palindromicRat_F_mul_E line 344
  36. def OAI.InternalCatalan.palindromicRatRow line 349
  37. theorem OAI.InternalCatalan.palindromicRatRow_successor line 353
  38. theorem OAI.InternalCatalan.palindromicRatRow_scale line 360
  39. theorem OAI.InternalCatalan.palindromicRatRow_expansion line 369
  40. theorem OAI.InternalCatalan.chebyshev_signed_laurent_eval line 404
  41. theorem OAI.InternalCatalan.palindromicRat_two_ne_zero line 444
  42. theorem OAI.InternalCatalan.palindromicRat_T_ne_zero line 453
  43. theorem OAI.InternalCatalan.palindromicRat_invT_sub_F_div_T line 458
  44. theorem OAI.InternalCatalan.palindromicRat_F_div_T_sq line 466
  45. theorem OAI.InternalCatalan.palindromicRat_chebyshev_signed line 472
  46. theorem OAI.InternalCatalan.palindromicRat_inverse_denominator_ne_zero line 506
  47. theorem OAI.InternalCatalan.palindromicRatStar_T line 516
  48. theorem OAI.InternalCatalan.palindromicRatStar_F line 526
  49. theorem OAI.InternalCatalan.palindromicRatStar_E line 536
  50. theorem OAI.InternalCatalan.palindromicRatStar_F_pow line 540
  51. theorem OAI.InternalCatalan.palindromicRatStar_eval₂ line 545
  52. theorem OAI.InternalCatalan.palindromicRatStar_eval₂_int line 553
  53. theorem OAI.InternalCatalan.palindromicRat_F_ne_zero line 566