OAI/NumberTheory/Catalan/Energy/BarrierTwoNormVPrefix096.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierV2_norm_term_49 line 11
2. theorem OAI.InternalCatalan.barrierV2_norm_term_50 line 34
3. theorem OAI.InternalCatalan.barrierV2_norm_term_51 line 57
4. theorem OAI.InternalCatalan.barrierV2_norm_term_52 line 80
5. theorem OAI.InternalCatalan.barrierV2_norm_term_53 line 103
6. theorem OAI.InternalCatalan.barrierV2_norm_term_54 line 126
7. theorem OAI.InternalCatalan.barrierV2_norm_term_55 line 149
8. theorem OAI.InternalCatalan.barrierV2_norm_term_56 line 172
9. theorem OAI.InternalCatalan.barrierV2_norm_block_56 line 195
10. theorem OAI.InternalCatalan.barrierV2_norm_prefix_56 line 203
11. theorem OAI.InternalCatalan.barrierV2_norm_term_57 line 226
12. theorem OAI.InternalCatalan.barrierV2_norm_term_58 line 249
13. theorem OAI.InternalCatalan.barrierV2_norm_term_59 line 272
14. theorem OAI.InternalCatalan.barrierV2_norm_term_60 line 295
15. theorem OAI.InternalCatalan.barrierV2_norm_term_61 line 318
16. theorem OAI.InternalCatalan.barrierV2_norm_term_62 line 341
17. theorem OAI.InternalCatalan.barrierV2_norm_term_63 line 364
18. theorem OAI.InternalCatalan.barrierV2_norm_term_64 line 387
19. theorem OAI.InternalCatalan.barrierV2_norm_block_64 line 410
20. theorem OAI.InternalCatalan.barrierV2_norm_prefix_64 line 418
21. theorem OAI.InternalCatalan.barrierV2_norm_term_65 line 441
22. theorem OAI.InternalCatalan.barrierV2_norm_term_66 line 464
23. theorem OAI.InternalCatalan.barrierV2_norm_term_67 line 487
24. theorem OAI.InternalCatalan.barrierV2_norm_term_68 line 510
25. theorem OAI.InternalCatalan.barrierV2_norm_term_69 line 533
26. theorem OAI.InternalCatalan.barrierV2_norm_term_70 line 556
27. theorem OAI.InternalCatalan.barrierV2_norm_term_71 line 579
28. theorem OAI.InternalCatalan.barrierV2_norm_term_72 line 602
29. theorem OAI.InternalCatalan.barrierV2_norm_block_72 line 625
30. theorem OAI.InternalCatalan.barrierV2_norm_prefix_72 line 633
31. theorem OAI.InternalCatalan.barrierV2_norm_term_73 line 656
32. theorem OAI.InternalCatalan.barrierV2_norm_term_74 line 679
33. theorem OAI.InternalCatalan.barrierV2_norm_term_75 line 702
34. theorem OAI.InternalCatalan.barrierV2_norm_term_76 line 725
35. theorem OAI.InternalCatalan.barrierV2_norm_term_77 line 748
36. theorem OAI.InternalCatalan.barrierV2_norm_term_78 line 771
37. theorem OAI.InternalCatalan.barrierV2_norm_term_79 line 794
38. theorem OAI.InternalCatalan.barrierV2_norm_term_80 line 817
39. theorem OAI.InternalCatalan.barrierV2_norm_block_80 line 840
40. theorem OAI.InternalCatalan.barrierV2_norm_prefix_80 line 848
41. theorem OAI.InternalCatalan.barrierV2_norm_term_81 line 871
42. theorem OAI.InternalCatalan.barrierV2_norm_term_82 line 894
43. theorem OAI.InternalCatalan.barrierV2_norm_term_83 line 917
44. theorem OAI.InternalCatalan.barrierV2_norm_term_84 line 940
45. theorem OAI.InternalCatalan.barrierV2_norm_term_85 line 963
46. theorem OAI.InternalCatalan.barrierV2_norm_term_86 line 986
47. theorem OAI.InternalCatalan.barrierV2_norm_term_87 line 1009
48. theorem OAI.InternalCatalan.barrierV2_norm_term_88 line 1032
49. theorem OAI.InternalCatalan.barrierV2_norm_block_88 line 1055
50. theorem OAI.InternalCatalan.barrierV2_norm_prefix_88 line 1063
51. theorem OAI.InternalCatalan.barrierV2_norm_term_89 line 1086
52. theorem OAI.InternalCatalan.barrierV2_norm_term_90 line 1109
53. theorem OAI.InternalCatalan.barrierV2_norm_term_91 line 1132
54. theorem OAI.InternalCatalan.barrierV2_norm_term_92 line 1155
55. theorem OAI.InternalCatalan.barrierV2_norm_term_93 line 1178
56. theorem OAI.InternalCatalan.barrierV2_norm_term_94 line 1201
57. theorem OAI.InternalCatalan.barrierV2_norm_term_95 line 1224
58. theorem OAI.InternalCatalan.barrierV2_norm_term_96 line 1247
59. theorem OAI.InternalCatalan.barrierV2_norm_block_96 line 1270
60. theorem OAI.InternalCatalan.barrierV2_norm_prefix_96 line 1278