OAI/NumberTheory/Catalan/Polynomial/CentralCoefficients.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.centralCoeff line 20
  2. def OAI.InternalCatalan.centralCoeffKernel line 23
  3. theorem OAI.InternalCatalan.centralCoeff_zero line 26
  4. theorem OAI.InternalCatalan.centralCoeffKernel_zero line 29
  5. theorem OAI.InternalCatalan.centralCoeffKernel_of_neg line 32
  6. theorem OAI.InternalCatalan.centralCoeffKernel_of_odd line 36
  7. theorem OAI.InternalCatalan.centralCoeffKernel_two_mul line 40
  8. def OAI.InternalCatalan.momentScalar line 47
  9. theorem OAI.InternalCatalan.momentScalar_zero line 50
  10. theorem OAI.InternalCatalan.momentScalar_even line 53
  11. theorem OAI.InternalCatalan.momentScalar_odd line 57
  12. def OAI.InternalCatalan.boundaryMinus line 60
  13. def OAI.InternalCatalan.boundaryPlus line 67
  14. theorem OAI.InternalCatalan.boundaryMinus_zero line 74
  15. theorem OAI.InternalCatalan.boundaryMinus_one line 75
  16. theorem OAI.InternalCatalan.boundaryPlus_zero line 76
  17. theorem OAI.InternalCatalan.boundaryPlus_one line 77
  18. theorem OAI.InternalCatalan.boundaryMinus_step line 79
  19. theorem OAI.InternalCatalan.boundaryPlus_step line 86
  20. theorem OAI.InternalCatalan.boundaryMinus_unique line 93
  21. theorem OAI.InternalCatalan.boundaryPlus_unique line 108
  22. def OAI.InternalCatalan.momentRat line 123
  23. theorem OAI.InternalCatalan.momentRat_of_le line 131
  24. theorem OAI.InternalCatalan.momentRat_of_lt line 136
  25. theorem OAI.InternalCatalan.momentRat_zero_right line 141
  26. theorem OAI.InternalCatalan.momentRat_zero_left line 144
  27. theorem OAI.InternalCatalan.momentRat_diagonal line 149
  28. theorem OAI.InternalCatalan.momentRat_step line 153
  29. def OAI.InternalCatalan.momentRatNegOne line 169
  30. theorem OAI.InternalCatalan.momentRatNegOne_eq line 171
  31. def OAI.InternalCatalan.harmonicRat line 174
  32. theorem OAI.InternalCatalan.harmonicRat_zero line 177
  33. theorem OAI.InternalCatalan.harmonicRat_succ line 180
  34. def OAI.InternalCatalan.zetaRat line 184
  35. theorem OAI.InternalCatalan.zetaRat_diagonal line 188
  36. theorem OAI.InternalCatalan.zetaRat_of_ne line 191
  37. theorem OAI.InternalCatalan.zetaRat_symm line 195
  38. theorem OAI.InternalCatalan.zetaRat_step line 204
  39. theorem OAI.InternalCatalan.centralCoeff_pos line 230
  40. theorem OAI.InternalCatalan.centralCoeff_ne_zero line 236
  41. theorem OAI.InternalCatalan.centralCoeff_step line 239
  42. def OAI.InternalCatalan.boundaryFactor line 252
  43. theorem OAI.InternalCatalan.boundaryFactor_even line 256
  44. theorem OAI.InternalCatalan.boundaryFactor_odd line 259
  45. theorem OAI.InternalCatalan.boundaryFactor_zero line 263
  46. theorem OAI.InternalCatalan.boundaryFactor_one line 266
  47. theorem OAI.InternalCatalan.boundaryFactor_pos line 269
  48. theorem OAI.InternalCatalan.boundaryFactor_ne_zero line 277
  49. theorem OAI.InternalCatalan.boundaryFactor_step line 280
  50. theorem OAI.InternalCatalan.boundaryFactor_ratio line 304