OAI/NumberTheory/Catalan/Energy/BarrierTwoNormPPrefix060.lean

GitHub source file

140 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierP2MainBase line 11
  2. theorem OAI.InternalCatalan.barrierConjugatePair_neg_star_power_re line 13
  3. def OAI.InternalCatalan.barrierP2CoefficientFormula line 27
  4. theorem OAI.InternalCatalan.barrierP2_eq_coefficientFormula line 36
  5. theorem OAI.InternalCatalan.barrierP2_exact_power_1 line 62
  6. theorem OAI.InternalCatalan.barrierP2_norm_term_1 line 66
  7. theorem OAI.InternalCatalan.barrierP2_exact_power_2 line 72
  8. theorem OAI.InternalCatalan.barrierP2_norm_term_2 line 79
  9. theorem OAI.InternalCatalan.barrierP2_exact_power_3 line 85
  10. theorem OAI.InternalCatalan.barrierP2_norm_term_3 line 92
  11. theorem OAI.InternalCatalan.barrierP2_exact_power_4 line 98
  12. theorem OAI.InternalCatalan.barrierP2_norm_term_4 line 105
  13. theorem OAI.InternalCatalan.barrierP2_exact_power_5 line 111
  14. theorem OAI.InternalCatalan.barrierP2_norm_term_5 line 118
  15. theorem OAI.InternalCatalan.barrierP2_exact_power_6 line 124
  16. theorem OAI.InternalCatalan.barrierP2_norm_term_6 line 131
  17. theorem OAI.InternalCatalan.barrierP2_exact_power_7 line 137
  18. theorem OAI.InternalCatalan.barrierP2_norm_term_7 line 144
  19. theorem OAI.InternalCatalan.barrierP2_exact_power_8 line 150
  20. theorem OAI.InternalCatalan.barrierP2_norm_term_8 line 157
  21. theorem OAI.InternalCatalan.barrierP2_norm_block_8 line 163
  22. theorem OAI.InternalCatalan.barrierP2_norm_prefix_8 line 171
  23. theorem OAI.InternalCatalan.barrierP2_exact_power_9 line 187
  24. theorem OAI.InternalCatalan.barrierP2_norm_term_9 line 194
  25. theorem OAI.InternalCatalan.barrierP2_exact_power_10 line 200
  26. theorem OAI.InternalCatalan.barrierP2_norm_term_10 line 207
  27. theorem OAI.InternalCatalan.barrierP2_exact_power_11 line 213
  28. theorem OAI.InternalCatalan.barrierP2_norm_term_11 line 220
  29. theorem OAI.InternalCatalan.barrierP2_exact_power_12 line 226
  30. theorem OAI.InternalCatalan.barrierP2_norm_term_12 line 233
  31. theorem OAI.InternalCatalan.barrierP2_exact_power_13 line 239
  32. theorem OAI.InternalCatalan.barrierP2_norm_term_13 line 246
  33. theorem OAI.InternalCatalan.barrierP2_exact_power_14 line 252
  34. theorem OAI.InternalCatalan.barrierP2_norm_term_14 line 259
  35. theorem OAI.InternalCatalan.barrierP2_exact_power_15 line 265
  36. theorem OAI.InternalCatalan.barrierP2_norm_term_15 line 272
  37. theorem OAI.InternalCatalan.barrierP2_exact_power_16 line 278
  38. theorem OAI.InternalCatalan.barrierP2_norm_term_16 line 285
  39. theorem OAI.InternalCatalan.barrierP2_norm_block_16 line 291
  40. theorem OAI.InternalCatalan.barrierP2_norm_prefix_16 line 299
  41. theorem OAI.InternalCatalan.barrierP2_exact_power_17 line 322
  42. theorem OAI.InternalCatalan.barrierP2_norm_term_17 line 329
  43. theorem OAI.InternalCatalan.barrierP2_exact_power_18 line 335
  44. theorem OAI.InternalCatalan.barrierP2_norm_term_18 line 342
  45. theorem OAI.InternalCatalan.barrierP2_exact_power_19 line 348
  46. theorem OAI.InternalCatalan.barrierP2_norm_term_19 line 355
  47. theorem OAI.InternalCatalan.barrierP2_exact_power_20 line 361
  48. theorem OAI.InternalCatalan.barrierP2_norm_term_20 line 368
  49. theorem OAI.InternalCatalan.barrierP2_exact_power_21 line 374
  50. theorem OAI.InternalCatalan.barrierP2_norm_term_21 line 381
  51. theorem OAI.InternalCatalan.barrierP2_exact_power_22 line 387
  52. theorem OAI.InternalCatalan.barrierP2_norm_term_22 line 394
  53. theorem OAI.InternalCatalan.barrierP2_exact_power_23 line 400
  54. theorem OAI.InternalCatalan.barrierP2_norm_term_23 line 407
  55. theorem OAI.InternalCatalan.barrierP2_exact_power_24 line 413
  56. theorem OAI.InternalCatalan.barrierP2_norm_term_24 line 420
  57. theorem OAI.InternalCatalan.barrierP2_norm_block_24 line 426
  58. theorem OAI.InternalCatalan.barrierP2_norm_prefix_24 line 434
  59. theorem OAI.InternalCatalan.barrierP2_exact_power_25 line 457
  60. theorem OAI.InternalCatalan.barrierP2_norm_term_25 line 464
  61. theorem OAI.InternalCatalan.barrierP2_exact_power_26 line 470
  62. theorem OAI.InternalCatalan.barrierP2_norm_term_26 line 477
  63. theorem OAI.InternalCatalan.barrierP2_exact_power_27 line 483
  64. theorem OAI.InternalCatalan.barrierP2_norm_term_27 line 490
  65. theorem OAI.InternalCatalan.barrierP2_exact_power_28 line 496
  66. theorem OAI.InternalCatalan.barrierP2_norm_term_28 line 503
  67. theorem OAI.InternalCatalan.barrierP2_exact_power_29 line 509
  68. theorem OAI.InternalCatalan.barrierP2_norm_term_29 line 516
  69. theorem OAI.InternalCatalan.barrierP2_exact_power_30 line 522
  70. theorem OAI.InternalCatalan.barrierP2_norm_term_30 line 529
  71. theorem OAI.InternalCatalan.barrierP2_exact_power_31 line 535
  72. theorem OAI.InternalCatalan.barrierP2_norm_term_31 line 542
  73. theorem OAI.InternalCatalan.barrierP2_exact_power_32 line 548
  74. theorem OAI.InternalCatalan.barrierP2_norm_term_32 line 555
  75. theorem OAI.InternalCatalan.barrierP2_norm_block_32 line 561
  76. theorem OAI.InternalCatalan.barrierP2_norm_prefix_32 line 569
  77. theorem OAI.InternalCatalan.barrierP2_exact_power_33 line 592
  78. theorem OAI.InternalCatalan.barrierP2_norm_term_33 line 599
  79. theorem OAI.InternalCatalan.barrierP2_exact_power_34 line 605
  80. theorem OAI.InternalCatalan.barrierP2_norm_term_34 line 612
  81. theorem OAI.InternalCatalan.barrierP2_exact_power_35 line 618
  82. theorem OAI.InternalCatalan.barrierP2_norm_term_35 line 625
  83. theorem OAI.InternalCatalan.barrierP2_exact_power_36 line 631
  84. theorem OAI.InternalCatalan.barrierP2_norm_term_36 line 638
  85. theorem OAI.InternalCatalan.barrierP2_exact_power_37 line 644
  86. theorem OAI.InternalCatalan.barrierP2_norm_term_37 line 651
  87. theorem OAI.InternalCatalan.barrierP2_exact_power_38 line 657
  88. theorem OAI.InternalCatalan.barrierP2_norm_term_38 line 664
  89. theorem OAI.InternalCatalan.barrierP2_exact_power_39 line 670
  90. theorem OAI.InternalCatalan.barrierP2_norm_term_39 line 677
  91. theorem OAI.InternalCatalan.barrierP2_exact_power_40 line 683
  92. theorem OAI.InternalCatalan.barrierP2_norm_term_40 line 690
  93. theorem OAI.InternalCatalan.barrierP2_norm_block_40 line 696
  94. theorem OAI.InternalCatalan.barrierP2_norm_prefix_40 line 704
  95. theorem OAI.InternalCatalan.barrierP2_exact_power_41 line 727
  96. theorem OAI.InternalCatalan.barrierP2_norm_term_41 line 734
  97. theorem OAI.InternalCatalan.barrierP2_exact_power_42 line 740
  98. theorem OAI.InternalCatalan.barrierP2_norm_term_42 line 747
  99. theorem OAI.InternalCatalan.barrierP2_exact_power_43 line 753
  100. theorem OAI.InternalCatalan.barrierP2_norm_term_43 line 760
  101. theorem OAI.InternalCatalan.barrierP2_exact_power_44 line 766
  102. theorem OAI.InternalCatalan.barrierP2_norm_term_44 line 773
  103. theorem OAI.InternalCatalan.barrierP2_exact_power_45 line 779
  104. theorem OAI.InternalCatalan.barrierP2_norm_term_45 line 786
  105. theorem OAI.InternalCatalan.barrierP2_exact_power_46 line 792
  106. theorem OAI.InternalCatalan.barrierP2_norm_term_46 line 799
  107. theorem OAI.InternalCatalan.barrierP2_exact_power_47 line 805
  108. theorem OAI.InternalCatalan.barrierP2_norm_term_47 line 812
  109. theorem OAI.InternalCatalan.barrierP2_exact_power_48 line 818
  110. theorem OAI.InternalCatalan.barrierP2_norm_term_48 line 825
  111. theorem OAI.InternalCatalan.barrierP2_norm_block_48 line 831
  112. theorem OAI.InternalCatalan.barrierP2_norm_prefix_48 line 839
  113. theorem OAI.InternalCatalan.barrierP2_exact_power_49 line 862
  114. theorem OAI.InternalCatalan.barrierP2_norm_term_49 line 869
  115. theorem OAI.InternalCatalan.barrierP2_exact_power_50 line 875
  116. theorem OAI.InternalCatalan.barrierP2_norm_term_50 line 882
  117. theorem OAI.InternalCatalan.barrierP2_exact_power_51 line 888
  118. theorem OAI.InternalCatalan.barrierP2_norm_term_51 line 895
  119. theorem OAI.InternalCatalan.barrierP2_exact_power_52 line 901
  120. theorem OAI.InternalCatalan.barrierP2_norm_term_52 line 908
  121. theorem OAI.InternalCatalan.barrierP2_exact_power_53 line 914
  122. theorem OAI.InternalCatalan.barrierP2_norm_term_53 line 921
  123. theorem OAI.InternalCatalan.barrierP2_exact_power_54 line 927
  124. theorem OAI.InternalCatalan.barrierP2_norm_term_54 line 934
  125. theorem OAI.InternalCatalan.barrierP2_exact_power_55 line 940
  126. theorem OAI.InternalCatalan.barrierP2_norm_term_55 line 947
  127. theorem OAI.InternalCatalan.barrierP2_exact_power_56 line 953
  128. theorem OAI.InternalCatalan.barrierP2_norm_term_56 line 960
  129. theorem OAI.InternalCatalan.barrierP2_norm_block_56 line 966
  130. theorem OAI.InternalCatalan.barrierP2_norm_prefix_56 line 974
  131. theorem OAI.InternalCatalan.barrierP2_exact_power_57 line 997
  132. theorem OAI.InternalCatalan.barrierP2_norm_term_57 line 1004
  133. theorem OAI.InternalCatalan.barrierP2_exact_power_58 line 1010
  134. theorem OAI.InternalCatalan.barrierP2_norm_term_58 line 1017
  135. theorem OAI.InternalCatalan.barrierP2_exact_power_59 line 1023
  136. theorem OAI.InternalCatalan.barrierP2_norm_term_59 line 1030
  137. theorem OAI.InternalCatalan.barrierP2_exact_power_60 line 1036
  138. theorem OAI.InternalCatalan.barrierP2_norm_term_60 line 1043
  139. theorem OAI.InternalCatalan.barrierP2_norm_block_60 line 1049
  140. theorem OAI.InternalCatalan.barrierP2_norm_prefix_60 line 1057