OAI/NumberTheory/Catalan/Estimates/ChebyshevContact.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.centralCoefficientMap line 14
  2. def OAI.InternalCatalan.centralFunctional line 19
  3. theorem OAI.InternalCatalan.centralFunctional_monomial line 22
  4. theorem OAI.InternalCatalan.centralFunctional_C_mul line 27
  5. theorem OAI.InternalCatalan.centralFunctional_X_mul line 32
  6. theorem OAI.InternalCatalan.centralFunctional_stein line 42
  7. theorem OAI.InternalCatalan.centralFunctional_T_zero line 63
  8. theorem OAI.InternalCatalan.centralFunctional_two_X_mul line 77
  9. theorem OAI.InternalCatalan.centralFunctional_T_tail line 82
  10. theorem OAI.InternalCatalan.rationalIntCast_apply line 136
  11. theorem OAI.InternalCatalan.centralFunctional_eq_sum_range line 139
  12. theorem OAI.InternalCatalan.reversedRow_centralFunctional line 152
  13. theorem OAI.InternalCatalan.reversedChebyshev_contact line 174