OAI/NumberTheory/Catalan/Energy/BarrierDescartesCoefficientDegree.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierDescartesTransform line 24
  2. theorem OAI.InternalCatalan.barrierDescartesTransform_eval line 29
  3. theorem OAI.InternalCatalan.barrierDescartesTransform_eval_eq_zero_iff line 45
  4. theorem OAI.InternalCatalan.barrierMobius_inverse line 52
  5. theorem OAI.InternalCatalan.barrierDescartesTransform_root_of_interval line 64
  6. theorem OAI.InternalCatalan.barrier_coeff_affine_pow line 76
  7. theorem OAI.InternalCatalan.barrierDescartesTransform_coeff line 90
  8. def OAI.InternalCatalan.barrierDescartesCoeffRat line 115
  9. theorem OAI.InternalCatalan.barrierDescartesTransform_coeff_rat line 121
  10. theorem OAI.InternalCatalan.barrierDescartes_interval_roots_card_le line 141
  11. theorem OAI.InternalCatalan.barrierDescartesTransform_derivative_eval_eq_zero line 177
  12. theorem OAI.InternalCatalan.barrierDescartesTransform_simple_root_pullback line 205
  13. theorem OAI.InternalCatalan.barrierDescartesTransform_interval_simple_root_pullback line 231
  14. theorem OAI.InternalCatalan.barrierDescartesTransform_rootMultiplicity_one_of_interval line 247
  15. theorem OAI.InternalCatalan.barrierDescartesTransform_coeff_zero_above line 263