OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.InternalCatalan.BarrierRationalPairRow line 14
  2. def OAI.InternalCatalan.barrierP2RealRows line 20
  3. def OAI.InternalCatalan.barrierP2PairRows line 23
  4. def OAI.InternalCatalan.barrierV2RealRows line 29
  5. def OAI.InternalCatalan.barrierV2PairRows line 34
  6. def OAI.InternalCatalan.barrierExpandRealRows line 40
  7. def OAI.InternalCatalan.barrierExpandPairRow line 43
  8. def OAI.InternalCatalan.barrierExpandPairRows line 46
  9. theorem OAI.InternalCatalan.barrierP2Tail_eq_grouped line 49
  10. theorem OAI.InternalCatalan.barrierV2Tail_eq_grouped line 53
  11. def OAI.InternalCatalan.barrierRealLinearQ line 59
  12. def OAI.InternalCatalan.barrierRealQuadraticQ line 61
  13. def OAI.InternalCatalan.barrierGroupedLinearQ line 63
  14. def OAI.InternalCatalan.barrierGroupedQuadraticQ line 68
  15. theorem OAI.InternalCatalan.barrierRealLinearQ_eval_complex line 73
  16. theorem OAI.InternalCatalan.barrierRealQuadraticQ_eval_complex line 79
  17. theorem OAI.InternalCatalan.barrierPairLinearQ_eval_complex line 86
  18. theorem OAI.InternalCatalan.barrierPairQuadraticQ_eval_complex line 95
  19. theorem OAI.InternalCatalan.barrier_prod_map_flatMap line 104
  20. theorem OAI.InternalCatalan.barrierGroupedLinearQ_eval_complex line 111
  21. theorem OAI.InternalCatalan.barrierGroupedQuadraticQ_eval_complex line 121
  22. def OAI.InternalCatalan.barrierP2QuadraticQ line 131
  23. def OAI.InternalCatalan.barrierV2LinearQ line 134
  24. def OAI.InternalCatalan.barrierV2QuadraticQ line 137
  25. theorem OAI.InternalCatalan.barrierP2QuadraticQ_eval_complex line 140
  26. theorem OAI.InternalCatalan.barrierV2LinearQ_eval_complex line 146
  27. theorem OAI.InternalCatalan.barrierV2QuadraticQ_eval_complex line 152
  28. def OAI.InternalCatalan.barrierCase2QX line 158
  29. def OAI.InternalCatalan.barrierCase2QY line 161
  30. theorem OAI.InternalCatalan.barrierCase2QX_eval_complex line 163
  31. theorem OAI.InternalCatalan.barrierCase2QY_eval_complex line 169
  32. theorem OAI.InternalCatalan.barrier_ratPolynomial_eval_complex line 174
  33. theorem OAI.InternalCatalan.barrierCase2QX_eval_ne_zero line 180
  34. theorem OAI.InternalCatalan.barrierCase2QY_eval_ne_zero line 188
  35. def OAI.InternalCatalan.barrierGroupedLinearTailValue line 198
  36. def OAI.InternalCatalan.barrierGroupedQuadraticTailValue line 206
  37. theorem OAI.InternalCatalan.barrierComplex_real line 215
  38. theorem OAI.InternalCatalan.barrier_realTailLinear_re line 219
  39. theorem OAI.InternalCatalan.barrier_realTailQuadratic_re line 232
  40. theorem OAI.InternalCatalan.barrier_list_map_sum_re line 246
  41. theorem OAI.InternalCatalan.barrier_list_flatMap_sum_re line 254
  42. theorem OAI.InternalCatalan.barrier_grouped_tail_sum_re line 264
  43. theorem OAI.InternalCatalan.barrierP2Tail_quadratic_sum_re_eq_grouped line 282
  44. theorem OAI.InternalCatalan.barrierV2Tail_linear_sum_re_eq_grouped line 294
  45. theorem OAI.InternalCatalan.barrierV2Tail_quadratic_sum_re_eq_grouped line 306
  46. def OAI.InternalCatalan.barrierLinearFractions line 318
  47. def OAI.InternalCatalan.barrierQuadraticFractions line 324
  48. def OAI.InternalCatalan.barrierScaleFractions line 330
  49. theorem OAI.InternalCatalan.barrierLinearFractions_product line 333
  50. theorem OAI.InternalCatalan.barrierQuadraticFractions_product line 339
  51. theorem OAI.InternalCatalan.barrierFractionProduct_append line 345
  52. theorem OAI.InternalCatalan.barrierScaleFractions_product line 349
  53. theorem OAI.InternalCatalan.barrierLinearFractions_sum line 353
  54. theorem OAI.InternalCatalan.barrierQuadraticFractions_sum line 360
  55. theorem OAI.InternalCatalan.barrierFractionSum_append line 367
  56. theorem OAI.InternalCatalan.barrierScaleFractions_sum line 371
  57. def OAI.InternalCatalan.barrierCase2XFractions line 379
  58. def OAI.InternalCatalan.barrierCase2YFractions line 386
  59. def OAI.InternalCatalan.barrierCase2XDerivativeFormula line 391
  60. def OAI.InternalCatalan.barrierCase2YDerivativeFormula line 400
  61. theorem OAI.InternalCatalan.barrierCase2XFractions_product line 406
  62. theorem OAI.InternalCatalan.barrierCase2YFractions_product line 415
  63. theorem OAI.InternalCatalan.barrierCase2XFractions_sum line 422
  64. theorem OAI.InternalCatalan.barrierCase2YFractions_sum line 431
  65. def OAI.InternalCatalan.barrierCase2AX line 440
  66. def OAI.InternalCatalan.barrierCase2AY line 441
  67. theorem OAI.InternalCatalan.barrierCase2AX_clears_denominator line 443
  68. theorem OAI.InternalCatalan.barrierCase2AY_clears_denominator line 453
  69. def OAI.InternalCatalan.barrierCase2AYExplicit line 463
  70. theorem OAI.InternalCatalan.barrier_case2_U_3 line 490

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:355 (same declaration text).

  71. theorem OAI.InternalCatalan.barrier_case2_U_4 line 494

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:359 (same declaration text).

  72. theorem OAI.InternalCatalan.barrier_case2_U_5 line 498

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:363 (same declaration text).

  73. theorem OAI.InternalCatalan.barrier_case2_U_6 line 502

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:367 (same declaration text).

  74. theorem OAI.InternalCatalan.barrier_case2_U_7 line 506

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:371 (same declaration text).

  75. theorem OAI.InternalCatalan.barrier_case2_U_8 line 510

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:375 (same declaration text).

  76. theorem OAI.InternalCatalan.barrier_case2_U_9 line 514

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean:379 (same declaration text).

  77. theorem OAI.InternalCatalan.barrierCase2AY_eq_explicit line 518
  78. theorem OAI.InternalCatalan.barrierCase2AY_natDegree line 534
  79. def OAI.InternalCatalan.barrierCase2AXExplicit line 539
  80. def OAI.InternalCatalan.barrierCase2AXCoefficient line 578
  81. def OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit line 581
  82. def OAI.InternalCatalan.barrierCase2PTailProductExplicit line 593
  83. theorem OAI.InternalCatalan.barrierCase2PTailNumerator_eq_explicit line 606
  84. theorem OAI.InternalCatalan.barrierCase2PTailProduct_eq_explicit line 618
  85. def OAI.InternalCatalan.barrierCase2AYCoefficient line 630
  86. theorem OAI.InternalCatalan.barrierCase2AY_eval_quarter_ne_zero line 633
  87. theorem OAI.InternalCatalan.barrierCase2AY_eval_half_ne_zero line 638
  88. theorem OAI.InternalCatalan.barrierCase2AY_eval_three_quarters_ne_zero line 643
  89. theorem OAI.InternalCatalan.barrierCase2AY_quarter_nonzero line 648
  90. theorem OAI.InternalCatalan.barrierCase2AXExplicit_coeff_35 line 655
  91. theorem OAI.InternalCatalan.barrierCase2AXExplicit_coeff_36 line 661