OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOneDescartesX0.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierFiniteUDerivative line 24
  2. def OAI.InternalCatalan.barrierFinitePowerDerivative line 28
  3. def OAI.InternalCatalan.barrierCase1QX line 32
  4. def OAI.InternalCatalan.barrierCase1QY line 34
  5. def OAI.InternalCatalan.barrierCase1AX line 36
  6. def OAI.InternalCatalan.barrierCase1AY line 44
  7. def OAI.InternalCatalan.barrierCase1XDerivativeFormula line 48
  8. def OAI.InternalCatalan.barrierCase1YDerivativeFormula line 54
  9. theorem OAI.InternalCatalan.barrierCase1QX_eval_ne_zero line 58
  10. theorem OAI.InternalCatalan.barrierCase1QY_eval_ne_zero line 64
  11. theorem OAI.InternalCatalan.barrierCase1AX_clears_denominator line 68
  12. theorem OAI.InternalCatalan.barrierCase1AY_clears_denominator line 78
  13. def OAI.InternalCatalan.barrierCase1AXExplicit line 93
  14. def OAI.InternalCatalan.barrierCase1AYExplicit line 109
  15. theorem OAI.InternalCatalan.barrier_U_3 line 121
  16. theorem OAI.InternalCatalan.barrier_U_4 line 125
  17. theorem OAI.InternalCatalan.barrier_U_5 line 129
  18. theorem OAI.InternalCatalan.barrier_U_6 line 133
  19. theorem OAI.InternalCatalan.barrier_U_7 line 137
  20. theorem OAI.InternalCatalan.barrierCase1AX_eq_explicit line 141
  21. theorem OAI.InternalCatalan.barrierCase1AX_natDegree line 151
  22. theorem OAI.InternalCatalan.barrierCase1AY_eq_explicit line 156
  23. theorem OAI.InternalCatalan.barrierCase1AY_natDegree line 166
  24. def OAI.InternalCatalan.barrierBracketLeft line 171
  25. def OAI.InternalCatalan.barrierBracketRight line 173
  26. def OAI.InternalCatalan.barrierCase1XBrackets line 175
  27. theorem OAI.InternalCatalan.barrierCase1AX_bracket_signs line 178
  28. theorem OAI.InternalCatalan.barrierCase1X_bracket_domain line 186
  29. def OAI.InternalCatalan.barrierCase1YBrackets line 193
  30. theorem OAI.InternalCatalan.barrierCase1AY_bracket_signs line 196
  31. theorem OAI.InternalCatalan.barrierCase1Y_bracket_domain line 204
  32. def OAI.InternalCatalan.barrierCase1AYTransformExplicit line 210
  33. theorem OAI.InternalCatalan.barrierCase1AY_transform_eq_explicit line 222
  34. theorem OAI.InternalCatalan.barrierCase1AY_transform_signVariations line 232
  35. theorem OAI.InternalCatalan.barrierCase1AY_transform_positive_roots_le line 243
  36. theorem OAI.InternalCatalan.barrierCase1AX_subdivision_nonzero line 254
  37. theorem OAI.InternalCatalan.barrierCase1AY_endpoint_nonzero line 261
  38. def OAI.InternalCatalan.barrierCase1AXCoefficient line 269
  39. theorem OAI.InternalCatalan.barrierCase1AX_coeff_small line 272
  40. theorem OAI.InternalCatalan.barrierCase1AX_transform_eval line 279
  41. theorem OAI.InternalCatalan.barrierBracketLeft_lt_right line 293
  42. theorem OAI.InternalCatalan.barrierCase1AX_root_in_each_bracket line 300
  43. theorem OAI.InternalCatalan.barrierCase1AY_root_in_each_bracket line 306
  44. def OAI.InternalCatalan.barrierCase1AXTransform0Explicit line 314
  45. theorem OAI.InternalCatalan.barrierCase1AX_transform0_eq_explicit line 330
  46. def OAI.InternalCatalan.barrierCase1AXTransform1Explicit line 342
  47. theorem OAI.InternalCatalan.barrierCase1AX_transform1_eq_explicit line 358
  48. def OAI.InternalCatalan.barrierCase1AXTransform2Explicit line 368
  49. theorem OAI.InternalCatalan.barrierCase1AX_transform2_eq_explicit line 384
  50. def OAI.InternalCatalan.barrierCase1AXTransform3Explicit line 394
  51. theorem OAI.InternalCatalan.barrierCase1AX_transform3_eq_explicit line 410
  52. theorem OAI.InternalCatalan.barrierCase1AY_interval_roots_card_le line 420
  53. theorem OAI.InternalCatalan.barrierCase1Y_bracket_subset_interval line 438
  54. theorem OAI.InternalCatalan.barrierCase1Y_brackets_disjoint line 447
  55. def OAI.InternalCatalan.barrierCase1YChosenRoot line 462
  56. theorem OAI.InternalCatalan.barrierCase1YChosenRoot_spec line 467
  57. def OAI.InternalCatalan.barrierCase1YChosenRoots line 475
  58. theorem OAI.InternalCatalan.barrierCase1YChosenRoots_card line 479
  59. theorem OAI.InternalCatalan.barrierCase1YChosenRoots_spec line 494
  60. theorem OAI.InternalCatalan.barrierCase1AY_root_mem_chosen line 504
  61. theorem OAI.InternalCatalan.barrierCase1AY_roots_exhausted line 519
  62. theorem OAI.InternalCatalan.barrierCase1AY_unique_root_in_bracket line 531
  63. theorem OAI.InternalCatalan.barrierCase1AX_transform0_signVariations line 549
  64. theorem OAI.InternalCatalan.barrierCase1AX_transform0_positive_roots_le line 560