OAI/Combinatorics/Sidorenko/Tail.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.lowerTailTuple line 9
  2. theorem OAI.SidorenkoCounterexample.lowerTailTuple_s line 10
  3. theorem OAI.SidorenkoCounterexample.lowerTailTuple_feasible line 12
  4. def OAI.SidorenkoCounterexample.lowerTailConstant line 17
  5. theorem OAI.SidorenkoCounterexample.lowerTailConstant_pos line 19
  6. theorem OAI.SidorenkoCounterexample.pairParameters_card_le line 21
  7. theorem OAI.SidorenkoCounterexample.pairFaceDensity_lower_tail line 26
  8. def OAI.SidorenkoCounterexample.FaceTailChoice line 63
  9. instance OAI.SidorenkoCounterexample.faceTailChoiceFintype line 66
  10. def OAI.SidorenkoCounterexample.faceTailTuple line 68
  11. def OAI.SidorenkoCounterexample.faceTailConstant line 72
  12. theorem OAI.SidorenkoCounterexample.faceTailConstant_pos line 76
  13. theorem OAI.SidorenkoCounterexample.faceTailTuple_c line 81
  14. theorem OAI.SidorenkoCounterexample.faceTailTuple_s line 83
  15. theorem OAI.SidorenkoCounterexample.faceTailTuple_feasible line 88
  16. def OAI.SidorenkoCounterexample.faceTailMajorant line 94
  17. theorem OAI.SidorenkoCounterexample.faceTailMajorant_true line 97
  18. theorem OAI.SidorenkoCounterexample.faceTailMajorant_false line 99
  19. theorem OAI.SidorenkoCounterexample.faceTailMajorant_nonneg line 104
  20. def OAI.SidorenkoCounterexample.profileS line 114
  21. def OAI.SidorenkoCounterexample.GeometricProfile line 115
  22. theorem OAI.SidorenkoCounterexample.PointProfile.faceLocal line 122
  23. theorem OAI.SidorenkoCounterexample.PointProfile.geometric line 131
  24. theorem OAI.SidorenkoCounterexample.profileCost_baseline line 156
  25. abbrev OAI.SidorenkoCounterexample.GlobalTailChoice line 170
  26. def OAI.SidorenkoCounterexample.globalTailTuple line 172
  27. def OAI.SidorenkoCounterexample.globalTailConstant line 175
  28. def OAI.SidorenkoCounterexample.globalTailGain line 177
  29. theorem OAI.SidorenkoCounterexample.globalTailConstant_nonneg line 179
  30. theorem OAI.SidorenkoCounterexample.globalTailTuple_feasible line 182
  31. theorem OAI.SidorenkoCounterexample.globalTailGain_cost line 189
  32. theorem OAI.SidorenkoCounterexample.prod_faceTailMajorant line 196
  33. def OAI.SidorenkoCounterexample.residualDirectConstant line 211
  34. def OAI.SidorenkoCounterexample.residualNondirectConstant line 213
  35. theorem OAI.SidorenkoCounterexample.residualDirectConstant_nonneg line 215
  36. theorem OAI.SidorenkoCounterexample.residualNondirectConstant_nonneg line 217
  37. theorem OAI.SidorenkoCounterexample.pairDimProfile_card_split line 224
  38. theorem OAI.SidorenkoCounterexample.pairDimProfile_residual_card_bound line 228
  39. theorem OAI.SidorenkoCounterexample.pointProfile_card_le_pair line 239
  40. def OAI.SidorenkoCounterexample.normalizedPointProfileCount line 244
  41. theorem OAI.SidorenkoCounterexample.normalizedPointProfileCount_nonneg line 247
  42. theorem OAI.SidorenkoCounterexample.lagrangianRealCard_pos line 249
  43. theorem OAI.SidorenkoCounterexample.normalizedPointProfileCount_exposure line 253
  44. theorem OAI.SidorenkoCounterexample.normalizedPointProfileCount_residual line 258
  45. theorem OAI.SidorenkoCounterexample.residual_triangular_sum_le line 270
  46. theorem OAI.SidorenkoCounterexample.singular_triangular_sum_pos line 277
  47. theorem OAI.SidorenkoCounterexample.globalTail_dichotomy line 282
  48. def OAI.SidorenkoCounterexample.profileTermMajorant line 302
  49. theorem OAI.SidorenkoCounterexample.profileTermMajorant_nonneg line 308
  50. theorem OAI.SidorenkoCounterexample.negative_rpow_tendsto_zero line 316
  51. theorem OAI.SidorenkoCounterexample.profileTermMajorant_tendsto_zero line 319
  52. theorem OAI.SidorenkoCounterexample.residual_gain_bound line 333
  53. theorem OAI.SidorenkoCounterexample.normalizedPointProfile_term_bound line 350
  54. def OAI.SidorenkoCounterexample.profileTailMajorant line 372
  55. theorem OAI.SidorenkoCounterexample.profileTailMajorant_tendsto_zero line 375
  56. theorem OAI.SidorenkoCounterexample.normalizedPointProfile_product_bound line 388
  57. abbrev OAI.SidorenkoCounterexample.ActiveCenterSet line 413
  58. def OAI.SidorenkoCounterexample.activeFaceDensity line 415
  59. theorem OAI.SidorenkoCounterexample.activeFaceDensity_nonneg line 420
  60. theorem OAI.SidorenkoCounterexample.lagrangian_card_pos line 424
  61. theorem OAI.SidorenkoCounterexample.activeFaceDensity_empty line 429
  62. theorem OAI.SidorenkoCounterexample.activeFaceDensity_singleton line 435
  63. theorem OAI.SidorenkoCounterexample.activeFaceDensity_pair line 450
  64. theorem OAI.SidorenkoCounterexample.activeFaceDensity_full line 460
  65. theorem OAI.SidorenkoCounterexample.one_le_lowerTailMajorant line 469
  66. theorem OAI.SidorenkoCounterexample.fin3_subsets line 485
  67. theorem OAI.SidorenkoCounterexample.activeFaceDensity_lower_bound line 488
  68. theorem OAI.SidorenkoCounterexample.activeFaceDensity_tail_bound line 508
  69. abbrev OAI.SidorenkoCounterexample.DimProfile line 531
  70. def OAI.SidorenkoCounterexample.DimProfile.c line 532
  71. def OAI.SidorenkoCounterexample.DimProfile.h line 533
  72. def OAI.SidorenkoCounterexample.profileActiveDensity line 537
  73. theorem OAI.SidorenkoCounterexample.profileActiveDensity_nonneg line 544
  74. theorem OAI.SidorenkoCounterexample.profileActiveDensity_bound line 551
  75. theorem OAI.SidorenkoCounterexample.profileTailMajorant_nonneg line 578
  76. def OAI.SidorenkoCounterexample.integratedTailMajorant line 582
  77. theorem OAI.SidorenkoCounterexample.integratedTailMajorant_tendsto_zero line 585
  78. def OAI.SidorenkoCounterexample.singularTailThreshold line 599
  79. theorem OAI.SidorenkoCounterexample.singularTailThreshold_large line 600
  80. theorem OAI.SidorenkoCounterexample.singularTailThreshold_dichotomy line 601
  81. theorem OAI.SidorenkoCounterexample.profileActiveDensity_tail_bound line 612
  82. def OAI.SidorenkoCounterexample.integratedActiveTail line 630
  83. theorem OAI.SidorenkoCounterexample.integratedActiveTail_nonneg line 635
  84. theorem OAI.SidorenkoCounterexample.integratedActiveTail_bound line 640
  85. theorem OAI.SidorenkoCounterexample.finite_inf_lagrangians_finrank_le line 667
  86. def OAI.SidorenkoCounterexample.configProfile line 676
  87. theorem OAI.SidorenkoCounterexample.configProfile_property line 684
  88. theorem OAI.SidorenkoCounterexample.configProfile_eq_iff line 688
  89. def OAI.SidorenkoCounterexample.actualSingularTail line 697
  90. theorem OAI.SidorenkoCounterexample.actualSingularTail_eq_integrated line 707
  91. theorem OAI.SidorenkoCounterexample.actualSingularTail_nonneg line 744
  92. theorem OAI.SidorenkoCounterexample.actualSingularTail_bound line 756