OAI/NumberTheory/Catalan/Energy/BarrierTwoNormVPrefix192.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierV2_norm_term_145 line 11
2. theorem OAI.InternalCatalan.barrierV2_norm_term_146 line 34
3. theorem OAI.InternalCatalan.barrierV2_norm_term_147 line 57
4. theorem OAI.InternalCatalan.barrierV2_norm_term_148 line 80
5. theorem OAI.InternalCatalan.barrierV2_norm_term_149 line 103
6. theorem OAI.InternalCatalan.barrierV2_norm_term_150 line 126
7. theorem OAI.InternalCatalan.barrierV2_norm_term_151 line 149
8. theorem OAI.InternalCatalan.barrierV2_norm_term_152 line 172
9. theorem OAI.InternalCatalan.barrierV2_norm_block_152 line 195
10. theorem OAI.InternalCatalan.barrierV2_norm_prefix_152 line 203
11. theorem OAI.InternalCatalan.barrierV2_norm_term_153 line 226
12. theorem OAI.InternalCatalan.barrierV2_norm_term_154 line 249
13. theorem OAI.InternalCatalan.barrierV2_norm_term_155 line 272
14. theorem OAI.InternalCatalan.barrierV2_norm_term_156 line 295
15. theorem OAI.InternalCatalan.barrierV2_norm_term_157 line 318
16. theorem OAI.InternalCatalan.barrierV2_norm_term_158 line 341
17. theorem OAI.InternalCatalan.barrierV2_norm_term_159 line 364
18. theorem OAI.InternalCatalan.barrierV2_norm_term_160 line 387
19. theorem OAI.InternalCatalan.barrierV2_norm_block_160 line 410
20. theorem OAI.InternalCatalan.barrierV2_norm_prefix_160 line 418
21. theorem OAI.InternalCatalan.barrierV2_norm_term_161 line 441
22. theorem OAI.InternalCatalan.barrierV2_norm_term_162 line 464
23. theorem OAI.InternalCatalan.barrierV2_norm_term_163 line 487
24. theorem OAI.InternalCatalan.barrierV2_norm_term_164 line 510
25. theorem OAI.InternalCatalan.barrierV2_norm_term_165 line 533
26. theorem OAI.InternalCatalan.barrierV2_norm_term_166 line 556
27. theorem OAI.InternalCatalan.barrierV2_norm_term_167 line 579
28. theorem OAI.InternalCatalan.barrierV2_norm_term_168 line 602
29. theorem OAI.InternalCatalan.barrierV2_norm_block_168 line 625
30. theorem OAI.InternalCatalan.barrierV2_norm_prefix_168 line 633
31. theorem OAI.InternalCatalan.barrierV2_norm_term_169 line 656
32. theorem OAI.InternalCatalan.barrierV2_norm_term_170 line 679
33. theorem OAI.InternalCatalan.barrierV2_norm_term_171 line 702
34. theorem OAI.InternalCatalan.barrierV2_norm_term_172 line 725
35. theorem OAI.InternalCatalan.barrierV2_norm_term_173 line 748
36. theorem OAI.InternalCatalan.barrierV2_norm_term_174 line 771
37. theorem OAI.InternalCatalan.barrierV2_norm_term_175 line 794
38. theorem OAI.InternalCatalan.barrierV2_norm_term_176 line 817
39. theorem OAI.InternalCatalan.barrierV2_norm_block_176 line 840
40. theorem OAI.InternalCatalan.barrierV2_norm_prefix_176 line 848
41. theorem OAI.InternalCatalan.barrierV2_norm_term_177 line 871
42. theorem OAI.InternalCatalan.barrierV2_norm_term_178 line 894
43. theorem OAI.InternalCatalan.barrierV2_norm_term_179 line 917
44. theorem OAI.InternalCatalan.barrierV2_norm_term_180 line 940
45. theorem OAI.InternalCatalan.barrierV2_norm_term_181 line 963
46. theorem OAI.InternalCatalan.barrierV2_norm_term_182 line 986
47. theorem OAI.InternalCatalan.barrierV2_norm_term_183 line 1009
48. theorem OAI.InternalCatalan.barrierV2_norm_term_184 line 1032
49. theorem OAI.InternalCatalan.barrierV2_norm_block_184 line 1055
50. theorem OAI.InternalCatalan.barrierV2_norm_prefix_184 line 1063
51. theorem OAI.InternalCatalan.barrierV2_norm_term_185 line 1086
52. theorem OAI.InternalCatalan.barrierV2_norm_term_186 line 1109
53. theorem OAI.InternalCatalan.barrierV2_norm_term_187 line 1132
54. theorem OAI.InternalCatalan.barrierV2_norm_term_188 line 1155
55. theorem OAI.InternalCatalan.barrierV2_norm_term_189 line 1178
56. theorem OAI.InternalCatalan.barrierV2_norm_term_190 line 1201
57. theorem OAI.InternalCatalan.barrierV2_norm_term_191 line 1224
58. theorem OAI.InternalCatalan.barrierV2_norm_term_192 line 1247
59. theorem OAI.InternalCatalan.barrierV2_norm_block_192 line 1270
60. theorem OAI.InternalCatalan.barrierV2_norm_prefix_192 line 1278