OAI/Combinatorics/Sidorenko/Exposure.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.SeqValid line 10
  2. abbrev OAI.SidorenkoCounterexample.ValidSeq line 16
  3. def OAI.SidorenkoCounterexample.validSeqSuccEquiv line 20
  4. theorem OAI.SidorenkoCounterexample.validSeq_card_bound line 42
  5. def OAI.SidorenkoCounterexample.faceVertex line 62
  6. def OAI.SidorenkoCounterexample.classFace line 63
  7. def OAI.SidorenkoCounterexample.classPoint line 64
  8. def OAI.SidorenkoCounterexample.classOldZero line 65
  9. def OAI.SidorenkoCounterexample.classOldOne line 66
  10. def OAI.SidorenkoCounterexample.classOldPair line 67
  11. def OAI.SidorenkoCounterexample.classNewPairZero line 68
  12. def OAI.SidorenkoCounterexample.classNewPairOne line 69
  13. def OAI.SidorenkoCounterexample.classParent line 70
  14. theorem OAI.SidorenkoCounterexample.faceVertex_correct line 72
  15. theorem OAI.SidorenkoCounterexample.classPoint_bijective line 73
  16. theorem OAI.SidorenkoCounterexample.classFace_injective line 74
  17. theorem OAI.SidorenkoCounterexample.classOldZero_lt line 75
  18. theorem OAI.SidorenkoCounterexample.classOldOne_lt line 76
  19. theorem OAI.SidorenkoCounterexample.classRoot_correct line 77
  20. theorem OAI.SidorenkoCounterexample.classStep_correct line 78
  21. theorem OAI.SidorenkoCounterexample.classOldPair_correct line 80
  22. theorem OAI.SidorenkoCounterexample.classNewPairZero_correct line 82
  23. theorem OAI.SidorenkoCounterexample.classNewPairOne_correct line 84
  24. theorem OAI.SidorenkoCounterexample.classParent_lt line 86
  25. theorem OAI.SidorenkoCounterexample.classOldPair_parent line 87
  26. theorem OAI.SidorenkoCounterexample.classOldPair_injective line 88
  27. def OAI.SidorenkoCounterexample.classContains line 89
  28. instance OAI.SidorenkoCounterexample.(instance at line 90) line 90
  29. def OAI.SidorenkoCounterexample.classInternal line 91
  30. instance OAI.SidorenkoCounterexample.(instance at line 92) line 92
  31. theorem OAI.SidorenkoCounterexample.classFace_occurs line 93
  32. theorem OAI.SidorenkoCounterexample.classInternal_occurs line 94
  33. theorem OAI.SidorenkoCounterexample.classOldPair_internal line 95
  34. theorem OAI.SidorenkoCounterexample.classStep_pairs line 96
  35. theorem OAI.SidorenkoCounterexample.classStep_pairs_distinct line 98
  36. theorem OAI.SidorenkoCounterexample.faceVertex_injective line 101
  37. theorem OAI.SidorenkoCounterexample.faceVertex_pairs line 102
  38. theorem OAI.SidorenkoCounterexample.classRootPairZero line 104
  39. theorem OAI.SidorenkoCounterexample.classRootPairOne line 105
  40. theorem OAI.SidorenkoCounterexample.classRootPairTwo line 106
  41. theorem OAI.SidorenkoCounterexample.classTree_occurs line 107
  42. theorem OAI.SidorenkoCounterexample.inverse_power_inequality line 111
  43. def OAI.SidorenkoCounterexample.naturalProfileCost line 119
  44. theorem OAI.SidorenkoCounterexample.tripleProfile_card_raw line 121
  45. theorem OAI.SidorenkoCounterexample.conditionalProfile_card_raw line 136
  46. def OAI.SidorenkoCounterexample.tupleThreeEquiv line 165
  47. def OAI.SidorenkoCounterexample.faceNaturalCost line 171
  48. theorem OAI.SidorenkoCounterexample.root_natural_cost line 173
  49. theorem OAI.SidorenkoCounterexample.step_natural_cost line 176
  50. def OAI.SidorenkoCounterexample.PointProfile line 195
  51. def OAI.SidorenkoCounterexample.LocalProfile line 198
  52. theorem OAI.SidorenkoCounterexample.PointProfile.local line 201
  53. def OAI.SidorenkoCounterexample.classRootConstraint line 221
  54. def OAI.SidorenkoCounterexample.classStepConstraint line 225
  55. def OAI.SidorenkoCounterexample.rootConstraintEquiv line 233
  56. def OAI.SidorenkoCounterexample.classStepBound line 240
  57. theorem OAI.SidorenkoCounterexample.classStepBound_nonneg line 245
  58. theorem OAI.SidorenkoCounterexample.classStep_card_bound line 251
  59. def OAI.SidorenkoCounterexample.classPrefix line 284
  60. theorem OAI.SidorenkoCounterexample.classPrefix_valid line 288
  61. def OAI.SidorenkoCounterexample.pointProfile_class_injection line 304
  62. theorem OAI.SidorenkoCounterexample.classRoot_card_bound line 316
  63. def OAI.SidorenkoCounterexample.classExponent line 328
  64. theorem OAI.SidorenkoCounterexample.classStepBound_product line 332
  65. theorem OAI.SidorenkoCounterexample.pointProfile_class_card_bound line 342
  66. theorem OAI.SidorenkoCounterexample.sum_class_faces line 373
  67. theorem OAI.SidorenkoCounterexample.sum_class_old_pairs line 386
  68. def OAI.SidorenkoCounterexample.profileCost line 397
  69. theorem OAI.SidorenkoCounterexample.sum_class_exponent line 399
  70. theorem OAI.SidorenkoCounterexample.pointProfile_card_bound line 409
  71. def OAI.SidorenkoCounterexample.ZeroSeqValid line 431
  72. abbrev OAI.SidorenkoCounterexample.ZeroValidSeq line 435
  73. def OAI.SidorenkoCounterexample.zeroValidSeqSuccEquiv line 437
  74. theorem OAI.SidorenkoCounterexample.zeroValidSeq_card_bound line 459
  75. def OAI.SidorenkoCounterexample.OrthogonalStep line 486
  76. abbrev OAI.SidorenkoCounterexample.OrthogonalTuple line 488
  77. theorem OAI.SidorenkoCounterexample.orthogonalSeq_independent line 490
  78. theorem OAI.SidorenkoCounterexample.orthogonalTuple_valid line 498
  79. def OAI.SidorenkoCounterexample.orthogonalTupleToSeq line 511
  80. def OAI.SidorenkoCounterexample.priorConstraintCount line 518
  81. theorem OAI.SidorenkoCounterexample.independent_orthogonal_card line 521
  82. theorem OAI.SidorenkoCounterexample.orthogonalStep_card_bound line 544
  83. theorem OAI.SidorenkoCounterexample.orthogonalTuple_card_bound line 560
  84. def OAI.SidorenkoCounterexample.constraintPairCount line 576
  85. theorem OAI.SidorenkoCounterexample.sum_priorConstraintCount line 579
  86. theorem OAI.SidorenkoCounterexample.orthogonalTuple_card_rpow line 594
  87. theorem OAI.SidorenkoCounterexample.nat_card_subtype_sum line 619
  88. theorem OAI.SidorenkoCounterexample.double_constraintPairCount line 623
  89. abbrev OAI.SidorenkoCounterexample.ConstrainedTuple line 647
  90. def OAI.SidorenkoCounterexample.enumeratedRelation line 649
  91. theorem OAI.SidorenkoCounterexample.enumeratedRelation_symm line 651
  92. theorem OAI.SidorenkoCounterexample.constrainedTuple_card_rpow line 656
  93. theorem OAI.SidorenkoCounterexample.independentTuples_card_lower line 704
  94. theorem OAI.SidorenkoCounterexample.containingLagrangian_card_rpow line 726
  95. abbrev OAI.SidorenkoCounterexample.FamilySpanStratum line 766
  96. def OAI.SidorenkoCounterexample.familySpanCoding line 768
  97. theorem OAI.SidorenkoCounterexample.familySpanCoding_injective line 773
  98. theorem OAI.SidorenkoCounterexample.familySpan_card_upper line 789
  99. abbrev OAI.SidorenkoCounterexample.DirectFamily line 821
  100. abbrev OAI.SidorenkoCounterexample.FamilyBases line 824
  101. theorem OAI.SidorenkoCounterexample.directFamilyBases_independent line 827
  102. def OAI.SidorenkoCounterexample.directBasisForget line 839
  103. theorem OAI.SidorenkoCounterexample.directBasisForget_injective line 845
  104. theorem OAI.SidorenkoCounterexample.familyBases_card_lower line 864
  105. theorem OAI.SidorenkoCounterexample.directFamily_card_bound line 872