OAI/Analysis/Triangular/Certificate/WaveJetsData.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.jetMultiplierBox line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.jetMultiplierBox_mem line 13
  3. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_0 line 30
  4. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_0_calc line 62
  5. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_0_mem line 65
  6. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_1 line 69
  7. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_1_calc line 101
  8. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_1_mem line 104
  9. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_2 line 108
  10. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_2_calc line 140
  11. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_2_mem line 143
  12. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_3 line 147
  13. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_3_calc line 179
  14. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_3_mem line 182
  15. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_4 line 186
  16. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_4_calc line 218
  17. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_4_mem line 221
  18. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_5 line 225
  19. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_5_calc line 257
  20. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_5_mem line 260
  21. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_6 line 264
  22. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_6_calc line 296
  23. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_6_mem line 299
  24. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_7 line 303
  25. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_7_calc line 335
  26. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_7_mem line 338
  27. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_8 line 342
  28. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_8_calc line 374
  29. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_8_mem line 377
  30. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_9 line 381
  31. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_9_calc line 413
  32. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_9_mem line 416
  33. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_10 line 420
  34. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_10_calc line 452
  35. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_10_mem line 455
  36. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_11 line 459
  37. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_11_calc line 491
  38. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_11_mem line 494
  39. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_12 line 498
  40. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_12_calc line 530
  41. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_12_mem line 533
  42. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_13 line 537
  43. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_13_calc line 569
  44. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_13_mem line 572
  45. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_14 line 576
  46. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_14_calc line 608
  47. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_14_mem line 611
  48. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_15 line 615
  49. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_15_calc line 647
  50. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_15_mem line 650
  51. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_16 line 654
  52. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_16_calc line 686
  53. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_16_mem line 689
  54. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_17 line 693
  55. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_17_calc line 725
  56. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_17_mem line 728
  57. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_18 line 732
  58. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_18_calc line 764
  59. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_18_mem line 767
  60. def OAI.AtomicTriangular.FiniteCertificate.jetTable0_19 line 771
  61. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_19_calc line 803
  62. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable0_19_mem line 806
  63. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_0 line 810
  64. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_0_calc line 842
  65. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_0_mem line 845
  66. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_1 line 849
  67. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_1_calc line 881
  68. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_1_mem line 884
  69. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_2 line 888
  70. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_2_calc line 920
  71. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_2_mem line 923
  72. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_3 line 927
  73. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_3_calc line 959
  74. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_3_mem line 962
  75. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_4 line 966
  76. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_4_calc line 998
  77. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_4_mem line 1001
  78. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_5 line 1005
  79. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_5_calc line 1037
  80. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_5_mem line 1040
  81. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_6 line 1044
  82. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_6_calc line 1076
  83. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_6_mem line 1079
  84. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_7 line 1083
  85. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_7_calc line 1115
  86. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_7_mem line 1118
  87. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_8 line 1122
  88. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_8_calc line 1154
  89. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_8_mem line 1157
  90. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_9 line 1161
  91. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_9_calc line 1193
  92. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_9_mem line 1196
  93. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_10 line 1200
  94. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_10_calc line 1232
  95. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_10_mem line 1235
  96. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_11 line 1239
  97. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_11_calc line 1271
  98. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_11_mem line 1274
  99. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_12 line 1278
  100. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_12_calc line 1310
  101. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_12_mem line 1313
  102. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_13 line 1317
  103. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_13_calc line 1349
  104. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_13_mem line 1352
  105. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_14 line 1356
  106. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_14_calc line 1388
  107. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_14_mem line 1391
  108. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_15 line 1395
  109. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_15_calc line 1427
  110. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_15_mem line 1430
  111. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_16 line 1434
  112. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_16_calc line 1466
  113. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_16_mem line 1469
  114. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_17 line 1473
  115. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_17_calc line 1505
  116. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_17_mem line 1508
  117. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_18 line 1512
  118. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_18_calc line 1544
  119. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_18_mem line 1547
  120. def OAI.AtomicTriangular.FiniteCertificate.jetTable1_19 line 1551
  121. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_19_calc line 1583
  122. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable1_19_mem line 1586
  123. def OAI.AtomicTriangular.FiniteCertificate.jetTable line 1590
  124. lemma OAI.AtomicTriangular.FiniteCertificate.jetTable_mem line 1593