OAI/NumberTheory/Catalan/Energy/BarrierTwoNormVPrefix048.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierV2_norm_term_1 line 11
2. theorem OAI.InternalCatalan.barrierV2_norm_term_2 line 35
3. theorem OAI.InternalCatalan.barrierV2_norm_term_3 line 59
4. theorem OAI.InternalCatalan.barrierV2_norm_term_4 line 83
5. theorem OAI.InternalCatalan.barrierV2_norm_term_5 line 107
6. theorem OAI.InternalCatalan.barrierV2_norm_term_6 line 131
7. theorem OAI.InternalCatalan.barrierV2_norm_term_7 line 155
8. theorem OAI.InternalCatalan.barrierV2_norm_term_8 line 179
9. theorem OAI.InternalCatalan.barrierV2_norm_block_8 line 203
10. theorem OAI.InternalCatalan.barrierV2_norm_prefix_8 line 211
11. theorem OAI.InternalCatalan.barrierV2_norm_term_9 line 227
12. theorem OAI.InternalCatalan.barrierV2_norm_term_10 line 251
13. theorem OAI.InternalCatalan.barrierV2_norm_term_11 line 275
14. theorem OAI.InternalCatalan.barrierV2_norm_term_12 line 298
15. theorem OAI.InternalCatalan.barrierV2_norm_term_13 line 321
16. theorem OAI.InternalCatalan.barrierV2_norm_term_14 line 344
17. theorem OAI.InternalCatalan.barrierV2_norm_term_15 line 368
18. theorem OAI.InternalCatalan.barrierV2_norm_term_16 line 391
19. theorem OAI.InternalCatalan.barrierV2_norm_block_16 line 414
20. theorem OAI.InternalCatalan.barrierV2_norm_prefix_16 line 422
21. theorem OAI.InternalCatalan.barrierV2_norm_term_17 line 445
22. theorem OAI.InternalCatalan.barrierV2_norm_term_18 line 468
23. theorem OAI.InternalCatalan.barrierV2_norm_term_19 line 492
24. theorem OAI.InternalCatalan.barrierV2_norm_term_20 line 515
25. theorem OAI.InternalCatalan.barrierV2_norm_term_21 line 538
26. theorem OAI.InternalCatalan.barrierV2_norm_term_22 line 561
27. theorem OAI.InternalCatalan.barrierV2_norm_term_23 line 585
28. theorem OAI.InternalCatalan.barrierV2_norm_term_24 line 608
29. theorem OAI.InternalCatalan.barrierV2_norm_block_24 line 631
30. theorem OAI.InternalCatalan.barrierV2_norm_prefix_24 line 639
31. theorem OAI.InternalCatalan.barrierV2_norm_term_25 line 662
32. theorem OAI.InternalCatalan.barrierV2_norm_term_26 line 685
33. theorem OAI.InternalCatalan.barrierV2_norm_term_27 line 709
34. theorem OAI.InternalCatalan.barrierV2_norm_term_28 line 732
35. theorem OAI.InternalCatalan.barrierV2_norm_term_29 line 755
36. theorem OAI.InternalCatalan.barrierV2_norm_term_30 line 778
37. theorem OAI.InternalCatalan.barrierV2_norm_term_31 line 802
38. theorem OAI.InternalCatalan.barrierV2_norm_term_32 line 825
39. theorem OAI.InternalCatalan.barrierV2_norm_block_32 line 848
40. theorem OAI.InternalCatalan.barrierV2_norm_prefix_32 line 856
41. theorem OAI.InternalCatalan.barrierV2_norm_term_33 line 879
42. theorem OAI.InternalCatalan.barrierV2_norm_term_34 line 902
43. theorem OAI.InternalCatalan.barrierV2_norm_term_35 line 926
44. theorem OAI.InternalCatalan.barrierV2_norm_term_36 line 949
45. theorem OAI.InternalCatalan.barrierV2_norm_term_37 line 972
46. theorem OAI.InternalCatalan.barrierV2_norm_term_38 line 995
47. theorem OAI.InternalCatalan.barrierV2_norm_term_39 line 1019
48. theorem OAI.InternalCatalan.barrierV2_norm_term_40 line 1042
49. theorem OAI.InternalCatalan.barrierV2_norm_block_40 line 1065
50. theorem OAI.InternalCatalan.barrierV2_norm_prefix_40 line 1073
51. theorem OAI.InternalCatalan.barrierV2_norm_term_41 line 1096
52. theorem OAI.InternalCatalan.barrierV2_norm_term_42 line 1119
53. theorem OAI.InternalCatalan.barrierV2_norm_term_43 line 1143
54. theorem OAI.InternalCatalan.barrierV2_norm_term_44 line 1166
55. theorem OAI.InternalCatalan.barrierV2_norm_term_45 line 1189
56. theorem OAI.InternalCatalan.barrierV2_norm_term_46 line 1212
57. theorem OAI.InternalCatalan.barrierV2_norm_term_47 line 1236
58. theorem OAI.InternalCatalan.barrierV2_norm_term_48 line 1259
59. theorem OAI.InternalCatalan.barrierV2_norm_block_48 line 1282
60. theorem OAI.InternalCatalan.barrierV2_norm_prefix_48 line 1290