OAI/Combinatorics/Sidorenko/Coefficients.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.labelProduct line 13
  2. def OAI.SidorenkoCounterexample.nonemptyLabels line 15
  3. lemma OAI.SidorenkoCounterexample.mem_nonemptyLabels line 16
  4. def OAI.SidorenkoCounterexample.activeCoefficient line 18
  5. lemma OAI.SidorenkoCounterexample.labelProduct_nonzero line 22
  6. lemma OAI.SidorenkoCounterexample.empty_propagation line 26
  7. lemma OAI.SidorenkoCounterexample.labelProduct_empty_dichotomy line 42
  8. lemma OAI.SidorenkoCounterexample.allCoefficient_eq line 70
  9. lemma OAI.SidorenkoCounterexample.activeCoefficient_unique line 87
  10. lemma OAI.SidorenkoCounterexample.identity_labels_forced line 100
  11. lemma OAI.SidorenkoCounterexample.identity_labelProduct line 128
  12. lemma OAI.SidorenkoCounterexample.pairCorners_nonempty line 140
  13. lemma OAI.SidorenkoCounterexample.identity_activeCoefficient line 146
  14. def OAI.SidorenkoCounterexample.activationEntry line 161
  15. lemma OAI.SidorenkoCounterexample.activationPhi_product line 163
  16. lemma OAI.SidorenkoCounterexample.activationEntry_abs line 175
  17. lemma OAI.SidorenkoCounterexample.bool_double_mean line 177
  18. lemma OAI.SidorenkoCounterexample.product_one_add_expansion line 181
  19. def OAI.SidorenkoCounterexample.faceSlot line 196
  20. def OAI.SidorenkoCounterexample.faceSide line 197
  21. theorem OAI.SidorenkoCounterexample.faceSlot_correct line 198
  22. theorem OAI.SidorenkoCounterexample.faceSide_correct line 199
  23. theorem OAI.SidorenkoCounterexample.faceSlot_side line 200
  24. theorem OAI.SidorenkoCounterexample.faceSide_slot line 201
  25. def OAI.SidorenkoCounterexample.occurrencePairEquiv line 203
  26. def OAI.SidorenkoCounterexample.pairCorner line 209
  27. lemma OAI.SidorenkoCounterexample.pairCorner_image_0 line 211
  28. lemma OAI.SidorenkoCounterexample.pairCorner_image_1 line 214
  29. lemma OAI.SidorenkoCounterexample.pairCorner_image_2 line 217
  30. lemma OAI.SidorenkoCounterexample.pairCorner_image_3 line 220
  31. lemma OAI.SidorenkoCounterexample.pairCorner_image_4 line 223
  32. lemma OAI.SidorenkoCounterexample.pairCorner_image_5 line 226
  33. lemma OAI.SidorenkoCounterexample.pairCorner_image_6 line 229
  34. lemma OAI.SidorenkoCounterexample.pairCorner_image_7 line 232
  35. lemma OAI.SidorenkoCounterexample.pairCorner_image_8 line 235
  36. lemma OAI.SidorenkoCounterexample.pairCorner_image_9 line 238
  37. lemma OAI.SidorenkoCounterexample.pairCorner_image_10 line 241
  38. lemma OAI.SidorenkoCounterexample.pairCorner_image_11 line 244
  39. lemma OAI.SidorenkoCounterexample.pairCorner_image_12 line 247
  40. lemma OAI.SidorenkoCounterexample.pairCorner_image_13 line 250
  41. lemma OAI.SidorenkoCounterexample.pairCorner_image_14 line 253
  42. lemma OAI.SidorenkoCounterexample.pairCorner_image_15 line 256
  43. lemma OAI.SidorenkoCounterexample.pairCorner_image_16 line 259
  44. lemma OAI.SidorenkoCounterexample.pairCorner_image_17 line 262
  45. lemma OAI.SidorenkoCounterexample.pairCorner_image_18 line 265
  46. lemma OAI.SidorenkoCounterexample.pairCorner_image_19 line 268
  47. lemma OAI.SidorenkoCounterexample.pairCorner_image_20 line 271
  48. lemma OAI.SidorenkoCounterexample.pairCorner_image_21 line 274
  49. lemma OAI.SidorenkoCounterexample.pairCorner_image_22 line 277
  50. lemma OAI.SidorenkoCounterexample.pairCorner_image_23 line 280
  51. lemma OAI.SidorenkoCounterexample.pairCorner_image_24 line 283
  52. lemma OAI.SidorenkoCounterexample.pairCorner_image_25 line 286
  53. lemma OAI.SidorenkoCounterexample.pairCorner_image_26 line 289
  54. lemma OAI.SidorenkoCounterexample.pairCorner_image_27 line 292
  55. lemma OAI.SidorenkoCounterexample.pairCorner_image_28 line 295
  56. lemma OAI.SidorenkoCounterexample.pairCorner_image_29 line 298
  57. lemma OAI.SidorenkoCounterexample.pairCorner_image_30 line 301
  58. lemma OAI.SidorenkoCounterexample.pairCorner_image_31 line 304
  59. lemma OAI.SidorenkoCounterexample.pairCorner_image_32 line 307
  60. theorem OAI.SidorenkoCounterexample.pairCorner_image line 310
  61. theorem OAI.SidorenkoCounterexample.pairCorner_inj line 345
  62. theorem OAI.SidorenkoCounterexample.pairCorners_product line 357
  63. lemma OAI.SidorenkoCounterexample.FiniteLaw.mean_expansion_product line 376
  64. lemma OAI.SidorenkoCounterexample.uniformMean_double_product line 384
  65. lemma OAI.SidorenkoCounterexample.activationMoment_product line 402
  66. lemma OAI.SidorenkoCounterexample.mean_activation_expansion line 405
  67. lemma OAI.SidorenkoCounterexample.labels_incidence_product line 426
  68. def OAI.SidorenkoCounterexample.expandedModel line 440
  69. lemma OAI.SidorenkoCounterexample.expandedModel_expansion line 443
  70. lemma OAI.SidorenkoCounterexample.expandedModel_mean line 451
  71. def OAI.SidorenkoCounterexample.coordinateActive line 461
  72. def OAI.SidorenkoCounterexample.coordinateSigns line 463
  73. lemma OAI.SidorenkoCounterexample.coordinateSigns_good line 466
  74. lemma OAI.SidorenkoCounterexample.coordinateSigns_real line 470
  75. lemma OAI.SidorenkoCounterexample.coordinate_factor line 475
  76. lemma OAI.SidorenkoCounterexample.coordinate_boolean_product line 485
  77. lemma OAI.SidorenkoCounterexample.coordinateModel_eq line 504
  78. lemma OAI.SidorenkoCounterexample.coordinateModels_product line 522
  79. def OAI.SidorenkoCounterexample.coordinateArrayEquiv line 540
  80. lemma OAI.SidorenkoCounterexample.uniformMean_coordinate_factor line 546
  81. lemma OAI.SidorenkoCounterexample.uniformMean_law_swap line 554
  82. lemma OAI.SidorenkoCounterexample.independent_mean_equiv line 561
  83. lemma OAI.SidorenkoCounterexample.independent_mean_prod line 574
  84. theorem OAI.SidorenkoCounterexample.faceVertex_mem line 600
  85. theorem OAI.SidorenkoCounterexample.faceVertex_surj line 604
  86. theorem OAI.SidorenkoCounterexample.corners_product line 612
  87. theorem OAI.SidorenkoCounterexample.faceSigns_good line 637
  88. theorem OAI.SidorenkoCounterexample.layerCorrelation_configuration line 645
  89. theorem OAI.SidorenkoCounterexample.pair_sub_face_iff line 664
  90. theorem OAI.SidorenkoCounterexample.product_facePair line 667
  91. theorem OAI.SidorenkoCounterexample.modelFace_polynomial line 680
  92. def OAI.SidorenkoCounterexample.pairBoolEquiv line 704
  93. theorem OAI.SidorenkoCounterexample.signModelCorrelation_configuration line 710
  94. def OAI.SidorenkoCounterexample.boolTestError line 735
  95. theorem OAI.SidorenkoCounterexample.boolTestError_tendsto line 740
  96. theorem OAI.SidorenkoCounterexample.varyingBoolTestError_tendsto line 748
  97. theorem OAI.SidorenkoCounterexample.rankLayerConvergence line 760
  98. theorem OAI.SidorenkoCounterexample.rankLayerLimit_proved line 776
  99. instance OAI.SidorenkoCounterexample.primeInfinity_neBot line 794