OAI/Combinatorics/Sidorenko/Activation.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SidorenkoCounterexample.ActCorner line 12
  2. def OAI.SidorenkoCounterexample.cornerPoint line 13
  3. def OAI.SidorenkoCounterexample.cornerPairL line 14
  4. def OAI.SidorenkoCounterexample.cornerPairR line 15
  5. def OAI.SidorenkoCounterexample.pairCorners line 16
  6. def OAI.SidorenkoCounterexample.cornerMax line 18
  7. def OAI.SidorenkoCounterexample.cornerGamma line 19
  8. theorem OAI.SidorenkoCounterexample.pairCorners_mem line 21
  9. def OAI.SidorenkoCounterexample.pairCornerTable line 23
  10. lemma OAI.SidorenkoCounterexample.pairCorners_table_0 line 56
  11. lemma OAI.SidorenkoCounterexample.pairCorners_table_1 line 57
  12. lemma OAI.SidorenkoCounterexample.pairCorners_table_2 line 58
  13. lemma OAI.SidorenkoCounterexample.pairCorners_table_3 line 59
  14. lemma OAI.SidorenkoCounterexample.pairCorners_table_4 line 60
  15. lemma OAI.SidorenkoCounterexample.pairCorners_table_5 line 61
  16. lemma OAI.SidorenkoCounterexample.pairCorners_table_6 line 62
  17. lemma OAI.SidorenkoCounterexample.pairCorners_table_7 line 63
  18. lemma OAI.SidorenkoCounterexample.pairCorners_table_8 line 64
  19. lemma OAI.SidorenkoCounterexample.pairCorners_table_9 line 65
  20. lemma OAI.SidorenkoCounterexample.pairCorners_table_10 line 66
  21. lemma OAI.SidorenkoCounterexample.pairCorners_table_11 line 67
  22. lemma OAI.SidorenkoCounterexample.pairCorners_table_12 line 68
  23. lemma OAI.SidorenkoCounterexample.pairCorners_table_13 line 69
  24. lemma OAI.SidorenkoCounterexample.pairCorners_table_14 line 70
  25. lemma OAI.SidorenkoCounterexample.pairCorners_table_15 line 71
  26. lemma OAI.SidorenkoCounterexample.pairCorners_table_16 line 72
  27. lemma OAI.SidorenkoCounterexample.pairCorners_table_17 line 73
  28. lemma OAI.SidorenkoCounterexample.pairCorners_table_18 line 74
  29. lemma OAI.SidorenkoCounterexample.pairCorners_table_19 line 75
  30. lemma OAI.SidorenkoCounterexample.pairCorners_table_20 line 76
  31. lemma OAI.SidorenkoCounterexample.pairCorners_table_21 line 77
  32. lemma OAI.SidorenkoCounterexample.pairCorners_table_22 line 78
  33. lemma OAI.SidorenkoCounterexample.pairCorners_table_23 line 79
  34. lemma OAI.SidorenkoCounterexample.pairCorners_table_24 line 80
  35. lemma OAI.SidorenkoCounterexample.pairCorners_table_25 line 81
  36. lemma OAI.SidorenkoCounterexample.pairCorners_table_26 line 82
  37. lemma OAI.SidorenkoCounterexample.pairCorners_table_27 line 83
  38. lemma OAI.SidorenkoCounterexample.pairCorners_table_28 line 84
  39. lemma OAI.SidorenkoCounterexample.pairCorners_table_29 line 85
  40. lemma OAI.SidorenkoCounterexample.pairCorners_table_30 line 86
  41. lemma OAI.SidorenkoCounterexample.pairCorners_table_31 line 87
  42. lemma OAI.SidorenkoCounterexample.pairCorners_table_32 line 88
  43. theorem OAI.SidorenkoCounterexample.pairCorners_table line 89
  44. theorem OAI.SidorenkoCounterexample.cornerPair_ne line 124
  45. lemma OAI.SidorenkoCounterexample.pairCorners_inter_0_0 line 129
  46. lemma OAI.SidorenkoCounterexample.pairCorners_inter_0_1 line 132
  47. lemma OAI.SidorenkoCounterexample.pairCorners_inter_0_2 line 135
  48. lemma OAI.SidorenkoCounterexample.pairCorners_inter_1_0 line 138
  49. lemma OAI.SidorenkoCounterexample.pairCorners_inter_1_1 line 141
  50. lemma OAI.SidorenkoCounterexample.pairCorners_inter_1_2 line 144
  51. lemma OAI.SidorenkoCounterexample.pairCorners_inter_2_0 line 147
  52. lemma OAI.SidorenkoCounterexample.pairCorners_inter_2_1 line 150
  53. lemma OAI.SidorenkoCounterexample.pairCorners_inter_2_2 line 153
  54. lemma OAI.SidorenkoCounterexample.pairCorners_inter_3_0 line 156
  55. lemma OAI.SidorenkoCounterexample.pairCorners_inter_3_1 line 159
  56. lemma OAI.SidorenkoCounterexample.pairCorners_inter_3_2 line 162
  57. lemma OAI.SidorenkoCounterexample.pairCorners_inter_4_0 line 165
  58. lemma OAI.SidorenkoCounterexample.pairCorners_inter_4_1 line 168
  59. lemma OAI.SidorenkoCounterexample.pairCorners_inter_4_2 line 171
  60. lemma OAI.SidorenkoCounterexample.pairCorners_inter_5_0 line 174
  61. lemma OAI.SidorenkoCounterexample.pairCorners_inter_5_1 line 177
  62. lemma OAI.SidorenkoCounterexample.pairCorners_inter_5_2 line 180
  63. lemma OAI.SidorenkoCounterexample.pairCorners_inter_6_0 line 183
  64. lemma OAI.SidorenkoCounterexample.pairCorners_inter_6_1 line 186
  65. lemma OAI.SidorenkoCounterexample.pairCorners_inter_6_2 line 189
  66. lemma OAI.SidorenkoCounterexample.pairCorners_inter_7_0 line 192
  67. lemma OAI.SidorenkoCounterexample.pairCorners_inter_7_1 line 195
  68. lemma OAI.SidorenkoCounterexample.pairCorners_inter_7_2 line 198
  69. lemma OAI.SidorenkoCounterexample.pairCorners_inter_8_0 line 201
  70. lemma OAI.SidorenkoCounterexample.pairCorners_inter_8_1 line 204
  71. lemma OAI.SidorenkoCounterexample.pairCorners_inter_8_2 line 207
  72. lemma OAI.SidorenkoCounterexample.pairCorners_inter_9_0 line 210
  73. lemma OAI.SidorenkoCounterexample.pairCorners_inter_9_1 line 213
  74. lemma OAI.SidorenkoCounterexample.pairCorners_inter_9_2 line 216
  75. lemma OAI.SidorenkoCounterexample.pairCorners_inter_10_0 line 219
  76. lemma OAI.SidorenkoCounterexample.pairCorners_inter_10_1 line 222
  77. lemma OAI.SidorenkoCounterexample.pairCorners_inter_10_2 line 225
  78. lemma OAI.SidorenkoCounterexample.pairCorners_inter_11_0 line 228
  79. lemma OAI.SidorenkoCounterexample.pairCorners_inter_11_1 line 231
  80. lemma OAI.SidorenkoCounterexample.pairCorners_inter_11_2 line 234
  81. lemma OAI.SidorenkoCounterexample.pairCorners_inter_12_0 line 237
  82. lemma OAI.SidorenkoCounterexample.pairCorners_inter_12_1 line 240
  83. lemma OAI.SidorenkoCounterexample.pairCorners_inter_12_2 line 243
  84. lemma OAI.SidorenkoCounterexample.pairCorners_inter_13_0 line 246
  85. lemma OAI.SidorenkoCounterexample.pairCorners_inter_13_1 line 249
  86. lemma OAI.SidorenkoCounterexample.pairCorners_inter_13_2 line 252
  87. lemma OAI.SidorenkoCounterexample.pairCorners_inter_14_0 line 255
  88. lemma OAI.SidorenkoCounterexample.pairCorners_inter_14_1 line 258
  89. lemma OAI.SidorenkoCounterexample.pairCorners_inter_14_2 line 261
  90. lemma OAI.SidorenkoCounterexample.pairCorners_inter_15_0 line 264
  91. lemma OAI.SidorenkoCounterexample.pairCorners_inter_15_1 line 267
  92. lemma OAI.SidorenkoCounterexample.pairCorners_inter_15_2 line 270
  93. lemma OAI.SidorenkoCounterexample.pairCorners_inter_16_0 line 273
  94. lemma OAI.SidorenkoCounterexample.pairCorners_inter_16_1 line 276
  95. lemma OAI.SidorenkoCounterexample.pairCorners_inter_16_2 line 279
  96. lemma OAI.SidorenkoCounterexample.pairCorners_inter_17_0 line 282
  97. lemma OAI.SidorenkoCounterexample.pairCorners_inter_17_1 line 285
  98. lemma OAI.SidorenkoCounterexample.pairCorners_inter_17_2 line 288
  99. lemma OAI.SidorenkoCounterexample.pairCorners_inter_18_0 line 291
  100. lemma OAI.SidorenkoCounterexample.pairCorners_inter_18_1 line 294
  101. lemma OAI.SidorenkoCounterexample.pairCorners_inter_18_2 line 297
  102. lemma OAI.SidorenkoCounterexample.pairCorners_inter_19_0 line 300
  103. lemma OAI.SidorenkoCounterexample.pairCorners_inter_19_1 line 303
  104. lemma OAI.SidorenkoCounterexample.pairCorners_inter_19_2 line 306
  105. lemma OAI.SidorenkoCounterexample.pairCorners_inter_20_0 line 309
  106. lemma OAI.SidorenkoCounterexample.pairCorners_inter_20_1 line 312
  107. lemma OAI.SidorenkoCounterexample.pairCorners_inter_20_2 line 315
  108. lemma OAI.SidorenkoCounterexample.pairCorners_inter_21_0 line 318
  109. lemma OAI.SidorenkoCounterexample.pairCorners_inter_21_1 line 321
  110. lemma OAI.SidorenkoCounterexample.pairCorners_inter_21_2 line 324
  111. theorem OAI.SidorenkoCounterexample.pairCorners_inter line 327
  112. theorem OAI.SidorenkoCounterexample.pairCorners_card line 396
  113. theorem OAI.SidorenkoCounterexample.cornerPairL_mem line 401
  114. theorem OAI.SidorenkoCounterexample.cornerPairR_mem line 402
  115. theorem OAI.SidorenkoCounterexample.cornerGamma_nonempty line 404
  116. theorem OAI.SidorenkoCounterexample.cornerMax_not_sub line 413
  117. lemma OAI.SidorenkoCounterexample.supportIntersect_0 line 419
  118. lemma OAI.SidorenkoCounterexample.corner_support_0 line 422
  119. lemma OAI.SidorenkoCounterexample.supportIntersect_1 line 429
  120. lemma OAI.SidorenkoCounterexample.corner_support_1 line 432
  121. lemma OAI.SidorenkoCounterexample.supportIntersect_2 line 439
  122. lemma OAI.SidorenkoCounterexample.corner_support_2 line 442
  123. lemma OAI.SidorenkoCounterexample.supportIntersect_3 line 449
  124. lemma OAI.SidorenkoCounterexample.corner_support_3 line 452
  125. lemma OAI.SidorenkoCounterexample.supportIntersect_4 line 459
  126. lemma OAI.SidorenkoCounterexample.corner_support_4 line 462
  127. lemma OAI.SidorenkoCounterexample.supportIntersect_5 line 469
  128. lemma OAI.SidorenkoCounterexample.corner_support_5 line 472
  129. lemma OAI.SidorenkoCounterexample.supportIntersect_6 line 479
  130. lemma OAI.SidorenkoCounterexample.corner_support_6 line 482
  131. lemma OAI.SidorenkoCounterexample.supportIntersect_7 line 489
  132. lemma OAI.SidorenkoCounterexample.corner_support_7 line 492
  133. lemma OAI.SidorenkoCounterexample.supportIntersect_8 line 499
  134. lemma OAI.SidorenkoCounterexample.corner_support_8 line 502
  135. lemma OAI.SidorenkoCounterexample.supportIntersect_9 line 509
  136. lemma OAI.SidorenkoCounterexample.corner_support_9 line 512
  137. lemma OAI.SidorenkoCounterexample.supportIntersect_10 line 519
  138. lemma OAI.SidorenkoCounterexample.corner_support_10 line 522
  139. lemma OAI.SidorenkoCounterexample.supportIntersect_11 line 529
  140. lemma OAI.SidorenkoCounterexample.corner_support_11 line 532
  141. lemma OAI.SidorenkoCounterexample.supportIntersect_12 line 539
  142. lemma OAI.SidorenkoCounterexample.corner_support_12 line 542
  143. lemma OAI.SidorenkoCounterexample.supportIntersect_13 line 549
  144. lemma OAI.SidorenkoCounterexample.corner_support_13 line 552
  145. lemma OAI.SidorenkoCounterexample.supportIntersect_14 line 559
  146. lemma OAI.SidorenkoCounterexample.corner_support_14 line 562
  147. lemma OAI.SidorenkoCounterexample.supportIntersect_15 line 569
  148. lemma OAI.SidorenkoCounterexample.corner_support_15 line 572
  149. lemma OAI.SidorenkoCounterexample.supportIntersect_16 line 579
  150. lemma OAI.SidorenkoCounterexample.corner_support_16 line 582
  151. lemma OAI.SidorenkoCounterexample.supportIntersect_17 line 589
  152. lemma OAI.SidorenkoCounterexample.corner_support_17 line 592
  153. lemma OAI.SidorenkoCounterexample.supportIntersect_18 line 599
  154. lemma OAI.SidorenkoCounterexample.corner_support_18 line 602
  155. lemma OAI.SidorenkoCounterexample.supportIntersect_19 line 609
  156. lemma OAI.SidorenkoCounterexample.corner_support_19 line 612
  157. lemma OAI.SidorenkoCounterexample.supportIntersect_20 line 619
  158. lemma OAI.SidorenkoCounterexample.corner_support_20 line 622
  159. lemma OAI.SidorenkoCounterexample.supportIntersect_21 line 629
  160. lemma OAI.SidorenkoCounterexample.corner_support_21 line 632
  161. lemma OAI.SidorenkoCounterexample.supportIntersect_22 line 639
  162. lemma OAI.SidorenkoCounterexample.corner_support_22 line 642
  163. lemma OAI.SidorenkoCounterexample.supportIntersect_23 line 649
  164. lemma OAI.SidorenkoCounterexample.corner_support_23 line 652
  165. lemma OAI.SidorenkoCounterexample.supportIntersect_24 line 659
  166. lemma OAI.SidorenkoCounterexample.corner_support_24 line 662
  167. lemma OAI.SidorenkoCounterexample.supportIntersect_25 line 669
  168. lemma OAI.SidorenkoCounterexample.corner_support_25 line 672
  169. lemma OAI.SidorenkoCounterexample.supportIntersect_26 line 679
  170. lemma OAI.SidorenkoCounterexample.corner_support_26 line 682
  171. lemma OAI.SidorenkoCounterexample.supportIntersect_27 line 689
  172. lemma OAI.SidorenkoCounterexample.corner_support_27 line 692
  173. lemma OAI.SidorenkoCounterexample.supportIntersect_28 line 699
  174. lemma OAI.SidorenkoCounterexample.corner_support_28 line 702
  175. lemma OAI.SidorenkoCounterexample.supportIntersect_29 line 709
  176. lemma OAI.SidorenkoCounterexample.corner_support_29 line 712
  177. lemma OAI.SidorenkoCounterexample.supportIntersect_30 line 719
  178. lemma OAI.SidorenkoCounterexample.corner_support_30 line 722
  179. lemma OAI.SidorenkoCounterexample.supportIntersect_31 line 729
  180. lemma OAI.SidorenkoCounterexample.corner_support_31 line 732
  181. lemma OAI.SidorenkoCounterexample.supportIntersect_32 line 739
  182. lemma OAI.SidorenkoCounterexample.corner_support_32 line 742
  183. theorem OAI.SidorenkoCounterexample.corner_support line 749
  184. theorem OAI.SidorenkoCounterexample.cornerGamma_sub line 785
  185. def OAI.SidorenkoCounterexample.cornerSigma line 788
  186. lemma OAI.SidorenkoCounterexample.cornerSigma_abs line 789
  187. def OAI.SidorenkoCounterexample.cornerLaw line 790
  188. lemma OAI.SidorenkoCounterexample.cornerLaw_zero line 793
  189. lemma OAI.SidorenkoCounterexample.cornerLaw_moment line 796
  190. lemma OAI.SidorenkoCounterexample.cornerLaw_support line 801
  191. lemma OAI.SidorenkoCounterexample.cornerLaw_disjoint line 807
  192. lemma OAI.SidorenkoCounterexample.cornerLaw_value line 810