OAI/Combinatorics/Sidorenko/GlobalMoments.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.slotLeft line 11
  2. def OAI.SidorenkoCounterexample.slotRight line 12
  3. theorem OAI.SidorenkoCounterexample.facePair_endpoints line 13
  4. theorem OAI.SidorenkoCounterexample.modelPair_mem line 17
  5. theorem OAI.SidorenkoCounterexample.face_pairs_image line 21
  6. theorem OAI.SidorenkoCounterexample.modelPair_all line 23
  7. def OAI.SidorenkoCounterexample.pairModelEquiv line 28
  8. def OAI.SidorenkoCounterexample.faceActive line 33
  9. def OAI.SidorenkoCounterexample.faceSigns line 35
  10. theorem OAI.SidorenkoCounterexample.fullTransverse_face line 38
  11. def OAI.SidorenkoCounterexample.boolFacePolynomial line 44
  12. theorem OAI.SidorenkoCounterexample.pairBool_eq_sign line 51
  13. theorem OAI.SidorenkoCounterexample.facePolynomial_bool line 57
  14. def OAI.SidorenkoCounterexample.configurationProduct line 80
  15. theorem OAI.SidorenkoCounterexample.configurationProduct_nonneg line 83
  16. def OAI.SidorenkoCounterexample.matrixSingularTail line 86
  17. def OAI.SidorenkoCounterexample.canonicalSingular line 91
  18. theorem OAI.SidorenkoCounterexample.canonicalSingular_chart line 95
  19. def OAI.SidorenkoCounterexample.canonicalConfiguration line 104
  20. theorem OAI.SidorenkoCounterexample.canonicalConfiguration_nonneg line 110
  21. theorem OAI.SidorenkoCounterexample.configuration_chart_bound line 114
  22. theorem OAI.SidorenkoCounterexample.actualSingularTail_uniform line 129
  23. theorem OAI.SidorenkoCounterexample.matrixSingularTail_bound line 146
  24. theorem OAI.SidorenkoCounterexample.canonicalTail_tendsto line 186
  25. theorem OAI.SidorenkoCounterexample.matrixSingularTail_tendsto line 206
  26. def OAI.SidorenkoCounterexample.configurationPolynomial line 243
  27. def OAI.SidorenkoCounterexample.globalBound line 246
  28. theorem OAI.SidorenkoCounterexample.globalBound_eight line 249
  29. theorem OAI.SidorenkoCounterexample.faceBound_le_global line 254
  30. theorem OAI.SidorenkoCounterexample.configuration_difference_bound line 260
  31. def OAI.SidorenkoCounterexample.transverseDifference line 277
  32. theorem OAI.SidorenkoCounterexample.transverseDifference_bound line 282
  33. theorem OAI.SidorenkoCounterexample.globalBound_tendsto line 299
  34. theorem OAI.SidorenkoCounterexample.transverseDifference_tendsto line 306
  35. def OAI.SidorenkoCounterexample.boolConfiguration line 329
  36. theorem OAI.SidorenkoCounterexample.boolFacePolynomial_abs_le line 333
  37. theorem OAI.SidorenkoCounterexample.boolConfiguration_abs_le line 349
  38. theorem OAI.SidorenkoCounterexample.configurationPolynomial_bool line 359
  39. def OAI.SidorenkoCounterexample.boolSingular line 367
  40. theorem OAI.SidorenkoCounterexample.boolSingular_bound line 372
  41. theorem OAI.SidorenkoCounterexample.configuration_mean_identity line 390
  42. theorem OAI.SidorenkoCounterexample.boolSingular_tendsto line 405
  43. theorem OAI.SidorenkoCounterexample.configuration_bool_tendsto line 416
  44. structure OAI.SidorenkoCounterexample.FiniteLaw line 439
  45. def OAI.SidorenkoCounterexample.FiniteLaw.mean line 446
  46. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_congr line 448
  47. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_const line 450
  48. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_add line 452
  49. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_sub line 454
  50. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_mul line 456
  51. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_mul_right line 458
  52. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_sum line 461
  53. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_finset_sum line 464
  54. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_nonneg line 466
  55. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_mono line 468
  56. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_bound line 470
  57. theorem OAI.SidorenkoCounterexample.FiniteLaw.abs_mean_le line 472
  58. def OAI.SidorenkoCounterexample.FiniteLaw.dirac line 477
  59. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_dirac line 481
  60. def OAI.SidorenkoCounterexample.FiniteLaw.uniform line 483
  61. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_uniform line 487
  62. def OAI.SidorenkoCounterexample.FiniteLaw.prod line 490
  63. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_prod line 494
  64. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_swap line 498
  65. def OAI.SidorenkoCounterexample.FiniteLaw.independent line 505
  66. theorem OAI.SidorenkoCounterexample.FiniteLaw.independent_mean_product line 510
  67. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_map_product line 515
  68. def OAI.SidorenkoCounterexample.FiniteLaw.mixture line 519
  69. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_mixture line 524
  70. def OAI.SidorenkoCounterexample.FiniteLaw.map line 528
  71. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_map line 533
  72. theorem OAI.SidorenkoCounterexample.FiniteLaw.mean_tendsto line 540
  73. theorem OAI.SidorenkoCounterexample.boolMonomial_asprod line 559
  74. theorem OAI.SidorenkoCounterexample.boolMonomial_abs line 564
  75. theorem OAI.SidorenkoCounterexample.boolMonomial_mul line 567
  76. theorem OAI.SidorenkoCounterexample.boolSign_mean line 577
  77. theorem OAI.SidorenkoCounterexample.boolMonomial_mean line 580
  78. theorem OAI.SidorenkoCounterexample.boolMonomial_orthog line 590
  79. def OAI.SidorenkoCounterexample.tiltLaw line 594
  80. theorem OAI.SidorenkoCounterexample.tiltLaw_mean line 606
  81. theorem OAI.SidorenkoCounterexample.tiltLaw_monomial line 612
  82. abbrev OAI.SidorenkoCounterexample.Activation line 619
  83. def OAI.SidorenkoCounterexample.activationPhi line 620
  84. theorem OAI.SidorenkoCounterexample.activationPhi_empty line 624
  85. theorem OAI.SidorenkoCounterexample.activationPhi_mul line 627
  86. theorem OAI.SidorenkoCounterexample.activationPhi_disjoint line 634
  87. def OAI.SidorenkoCounterexample.branchLaw line 639
  88. theorem OAI.SidorenkoCounterexample.branchLaw_phi line 642
  89. theorem OAI.SidorenkoCounterexample.branchLaw_second line 651
  90. def OAI.SidorenkoCounterexample.baseActivation line 663
  91. theorem OAI.SidorenkoCounterexample.baseActivation_zero line 667
  92. def OAI.SidorenkoCounterexample.activationMoment line 675
  93. theorem OAI.SidorenkoCounterexample.activationMoment_empty line 678
  94. theorem OAI.SidorenkoCounterexample.activationMoment_disjoint line 681
  95. theorem OAI.SidorenkoCounterexample.baseActivation_moment line 688