OAI/NumberTheory/Catalan/Energy/BarrierTwoNormVPrefix144.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierV2_norm_term_97 line 11
2. theorem OAI.InternalCatalan.barrierV2_norm_term_98 line 34
3. theorem OAI.InternalCatalan.barrierV2_norm_term_99 line 58
4. theorem OAI.InternalCatalan.barrierV2_norm_term_100 line 82
5. theorem OAI.InternalCatalan.barrierV2_norm_term_101 line 105
6. theorem OAI.InternalCatalan.barrierV2_norm_term_102 line 128
7. theorem OAI.InternalCatalan.barrierV2_norm_term_103 line 152
8. theorem OAI.InternalCatalan.barrierV2_norm_term_104 line 176
9. theorem OAI.InternalCatalan.barrierV2_norm_block_104 line 199
10. theorem OAI.InternalCatalan.barrierV2_norm_prefix_104 line 207
11. theorem OAI.InternalCatalan.barrierV2_norm_term_105 line 230
12. theorem OAI.InternalCatalan.barrierV2_norm_term_106 line 253
13. theorem OAI.InternalCatalan.barrierV2_norm_term_107 line 277
14. theorem OAI.InternalCatalan.barrierV2_norm_term_108 line 301
15. theorem OAI.InternalCatalan.barrierV2_norm_term_109 line 324
16. theorem OAI.InternalCatalan.barrierV2_norm_term_110 line 347
17. theorem OAI.InternalCatalan.barrierV2_norm_term_111 line 371
18. theorem OAI.InternalCatalan.barrierV2_norm_term_112 line 395
19. theorem OAI.InternalCatalan.barrierV2_norm_block_112 line 418
20. theorem OAI.InternalCatalan.barrierV2_norm_prefix_112 line 426
21. theorem OAI.InternalCatalan.barrierV2_norm_term_113 line 449
22. theorem OAI.InternalCatalan.barrierV2_norm_term_114 line 472
23. theorem OAI.InternalCatalan.barrierV2_norm_term_115 line 496
24. theorem OAI.InternalCatalan.barrierV2_norm_term_116 line 520
25. theorem OAI.InternalCatalan.barrierV2_norm_term_117 line 543
26. theorem OAI.InternalCatalan.barrierV2_norm_term_118 line 566
27. theorem OAI.InternalCatalan.barrierV2_norm_term_119 line 590
28. theorem OAI.InternalCatalan.barrierV2_norm_term_120 line 614
29. theorem OAI.InternalCatalan.barrierV2_norm_block_120 line 637
30. theorem OAI.InternalCatalan.barrierV2_norm_prefix_120 line 645
31. theorem OAI.InternalCatalan.barrierV2_norm_term_121 line 668
32. theorem OAI.InternalCatalan.barrierV2_norm_term_122 line 691
33. theorem OAI.InternalCatalan.barrierV2_norm_term_123 line 715
34. theorem OAI.InternalCatalan.barrierV2_norm_term_124 line 739
35. theorem OAI.InternalCatalan.barrierV2_norm_term_125 line 762
36. theorem OAI.InternalCatalan.barrierV2_norm_term_126 line 785
37. theorem OAI.InternalCatalan.barrierV2_norm_term_127 line 809
38. theorem OAI.InternalCatalan.barrierV2_norm_term_128 line 833
39. theorem OAI.InternalCatalan.barrierV2_norm_block_128 line 856
40. theorem OAI.InternalCatalan.barrierV2_norm_prefix_128 line 864
41. theorem OAI.InternalCatalan.barrierV2_norm_term_129 line 887
42. theorem OAI.InternalCatalan.barrierV2_norm_term_130 line 910
43. theorem OAI.InternalCatalan.barrierV2_norm_term_131 line 934
44. theorem OAI.InternalCatalan.barrierV2_norm_term_132 line 958
45. theorem OAI.InternalCatalan.barrierV2_norm_term_133 line 981
46. theorem OAI.InternalCatalan.barrierV2_norm_term_134 line 1004
47. theorem OAI.InternalCatalan.barrierV2_norm_term_135 line 1028
48. theorem OAI.InternalCatalan.barrierV2_norm_term_136 line 1052
49. theorem OAI.InternalCatalan.barrierV2_norm_block_136 line 1075
50. theorem OAI.InternalCatalan.barrierV2_norm_prefix_136 line 1083
51. theorem OAI.InternalCatalan.barrierV2_norm_term_137 line 1106
52. theorem OAI.InternalCatalan.barrierV2_norm_term_138 line 1129
53. theorem OAI.InternalCatalan.barrierV2_norm_term_139 line 1153
54. theorem OAI.InternalCatalan.barrierV2_norm_term_140 line 1177
55. theorem OAI.InternalCatalan.barrierV2_norm_term_141 line 1200
56. theorem OAI.InternalCatalan.barrierV2_norm_term_142 line 1223
57. theorem OAI.InternalCatalan.barrierV2_norm_term_143 line 1247
58. theorem OAI.InternalCatalan.barrierV2_norm_term_144 line 1271
59. theorem OAI.InternalCatalan.barrierV2_norm_block_144 line 1294
60. theorem OAI.InternalCatalan.barrierV2_norm_prefix_144 line 1302