OAI/Combinatorics/Progressions/FixedDensity/OrderedRemoval.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.HasDenseAPCount line 12
  2. def OAI.Erdos3.FixedDensity.HasWeightedAPCount line 18
  3. def OAI.Erdos3.FixedDensity.HasUniformDenseAPCount line 26
  4. def OAI.Erdos3.FixedDensity.HasUniformWeightedAPCount line 29
  5. theorem OAI.Erdos3.FixedDensity.weightedAPCount_of_denseAPCount line 32
  6. abbrev OAI.Erdos3.FixedDensity.SimplexHypergraph.DeletionFamily line 105
  7. def OAI.Erdos3.FixedDensity.SimplexHypergraph.deleteEdges line 108
  8. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deleteEdges_edge line 116
  9. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.mem_deleteEdges_simplexFinset line 125
  10. def OAI.Erdos3.FixedDensity.SimplexHypergraph.IsSimplexFree line 135
  11. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.isSimplexFree_iff line 139
  12. def OAI.Erdos3.FixedDensity.SimplexHypergraph.emptyDeletion line 150
  13. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.mem_emptyDeletion line 155
  14. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deleteEdges_empty_simplexFinset line 161
  15. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deleteEdges_simplexFinset_antitone line 170
  16. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.IsSimplexCover.mono line 181
  17. def OAI.Erdos3.FixedDensity.SimplexHypergraph.IsEdgeDeletion line 192
  18. def OAI.Erdos3.FixedDensity.SimplexHypergraph.trimDeletion line 197
  19. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.trimDeletion_isEdgeDeletion line 204
  20. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.trimDeletion_subset line 212
  21. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.IsSimplexCover.trim line 220
  22. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.trimDeletion_simplexFinset line 232
  23. def OAI.Erdos3.FixedDensity.SimplexHypergraph.fullEdgeDeletion line 251
  24. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.fullEdgeDeletion_isEdgeDeletion line 256
  25. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.fullEdgeDeletion_isSimplexCover line 262
  26. def OAI.Erdos3.FixedDensity.SimplexHypergraph.projectedSimplexDeletion line 273
  27. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.projectedSimplexDeletion_isEdgeDeletion line 280
  28. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.projectedSimplexDeletion_isSimplexCover line 290
  29. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.card_projectedSimplexDeletion_le line 300
  30. def OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount line 308
  31. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount_empty line 313
  32. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount_mono line 317
  33. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount_le_of_card_le line 325
  34. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount_trim_le line 337
  35. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount_projectedSimplexDeletion_le line 344
  36. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.exists_simplexCover_card_le_simplexFinset line 358
  37. def OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCapacity line 372
  38. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.card_deletedVector_fin line 377
  39. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCapacity_fin line 384
  40. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionCount_le_capacity line 389
  41. def OAI.Erdos3.FixedDensity.SimplexHypergraph.colorDeletionDensity line 397
  42. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.colorDeletionDensity_nonneg line 403
  43. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.colorDeletionDensity_le_one line 409
  44. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.colorDeletionDensity_fin line 418
  45. def OAI.Erdos3.FixedDensity.SimplexHypergraph.normalizedDeletionCost line 426
  46. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.normalizedDeletionCost_nonneg line 431
  47. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.normalizedDeletionCost_le_one line 437
  48. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.normalizedDeletionCost_mono line 445
  49. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.normalizedDeletionCost_trim_le line 455
  50. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.normalizedDeletionCost_empty line 463
  51. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.exists_minimum_simplexCover line 468
  52. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.exists_minimum_normalized_simplexCover line 501
  53. def OAI.Erdos3.FixedDensity.NoSimplexAfterDeleting line 521
  54. theorem OAI.Erdos3.FixedDensity.isSimplexCover_iff_noSimplexAfterDeleting line 527
  55. theorem OAI.Erdos3.FixedDensity.NoSimplexAfterDeleting.mono line 554
  56. theorem OAI.Erdos3.FixedDensity.emptyDeletion_isSimplexCover_iff line 567
  57. def OAI.Erdos3.FixedDensity.apSetHypergraph line 588
  58. theorem OAI.Erdos3.FixedDensity.apSetHypergraph_edge line 593
  59. theorem OAI.Erdos3.FixedDensity.apSetHypergraph_toWeighted_edgeWeight line 602
  60. theorem OAI.Erdos3.FixedDensity.apSetHypergraph_simplexCount_eq_cyclicAPCount line 617
  61. abbrev OAI.Erdos3.FixedDensity.DiagonalAPParameter line 631
  62. def OAI.Erdos3.FixedDensity.diagonalAPSimplex line 635
  63. theorem OAI.Erdos3.FixedDensity.simplexCoordinateSum_diagonalAPSimplex line 642
  64. theorem OAI.Erdos3.FixedDensity.simplexCoordinateMoment_diagonalAPSimplex line 650
  65. theorem OAI.Erdos3.FixedDensity.apSimplexForm_diagonalAPSimplex line 658
  66. theorem OAI.Erdos3.FixedDensity.diagonalAPSimplex_mem_simplexFinset line 670
  67. theorem OAI.Erdos3.FixedDensity.diagonalAPSimplex_injective line 683
  68. def OAI.Erdos3.FixedDensity.deletedVectorToFinTuple line 696
  69. theorem OAI.Erdos3.FixedDensity.deletedVectorToFinTuple_deleteCoordinate line 703
  70. theorem OAI.Erdos3.FixedDensity.eq_of_deletedVectorToFinTuple_eq_of_sum_eq line 710
  71. def OAI.Erdos3.FixedDensity.SimplexHypergraph.deletionSlotFinset line 762
  72. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.mem_deletionSlotFinset line 772
  73. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.card_deletionSlotFinset_le_deletionCount line 786
  74. def OAI.Erdos3.FixedDensity.diagonalCoverColor line 807
  75. theorem OAI.Erdos3.FixedDensity.diagonalCoverColor_mem line 821
  76. def OAI.Erdos3.FixedDensity.diagonalCoveredSlot line 836
  77. theorem OAI.Erdos3.FixedDensity.diagonalCoveredSlot_mem_deletionSlotFinset line 849
  78. theorem OAI.Erdos3.FixedDensity.diagonalCoveredSlot_injective line 866
  79. theorem OAI.Erdos3.FixedDensity.card_diagonalAPParameter line 888
  80. theorem OAI.Erdos3.FixedDensity.card_diagonalAPParameter_le_deletionCount line 894
  81. theorem OAI.Erdos3.FixedDensity.deletionCapacity_zmod line 923
  82. theorem OAI.Erdos3.FixedDensity.mean_finsetIndicator_div_le_normalizedDeletionCost line 931
  83. def OAI.Erdos3.FixedDensity.HasUniformCyclicPartiteSimplexRemoval line 965
  84. theorem OAI.Erdos3.FixedDensity.exists_uniformDenseAPCount_of_simplexRemoval line 979
  85. theorem OAI.Erdos3.FixedDensity.exists_uniformWeightedAPCount_of_simplexRemoval line 1020
  86. def OAI.Erdos3.FixedDensity.orderedFacet line 1046
  87. def OAI.Erdos3.FixedDensity.orderedFacetEquiv line 1050
  88. theorem OAI.Erdos3.FixedDensity.orderedFacetEquiv_apply line 1062
  89. theorem OAI.Erdos3.FixedDensity.deletedVectorToFinTuple_finTupleToDeletedVector line 1081
  90. theorem OAI.Erdos3.FixedDensity.finTupleToDeletedVector_deletedVectorToFinTuple line 1090
  91. def OAI.Erdos3.FixedDensity.deletedVectorFinTupleEquiv line 1101
  92. theorem OAI.Erdos3.FixedDensity.deletedVectorToFinTuple_deleteCoordinate_eq_orderedFaceTuple line 1111
  93. theorem OAI.Erdos3.FixedDensity.finTupleToDeletedVector_orderedFaceTuple line 1119
  94. def OAI.Erdos3.FixedDensity.SimplexHypergraph.toOrderedPattern line 1130
  95. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toOrderedPattern_edge_orderedFacet line 1139
  96. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toOrderedPattern_isOccurrence_iff line 1156
  97. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toOrderedPattern_occurrenceFinset line 1176
  98. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.toOrderedPattern_patternCount line 1186
  99. def OAI.Erdos3.FixedDensity.orderedDeletionToSimplex line 1197
  100. theorem OAI.Erdos3.FixedDensity.mem_orderedDeletionToSimplex_iff line 1209
  101. theorem OAI.Erdos3.FixedDensity.card_orderedDeletionToSimplex line 1229
  102. theorem OAI.Erdos3.FixedDensity.SimplexHypergraph.isSimplexCover_orderedDeletionToSimplex line 1244
  103. theorem OAI.Erdos3.FixedDensity.colorDeletionDensity_orderedDeletionToSimplex line 1267
  104. theorem OAI.Erdos3.FixedDensity.normalizedDeletionCost_orderedDeletionToSimplex_le line 1287
  105. theorem OAI.Erdos3.FixedDensity.hasUniformCyclicPartiteSimplexRemoval_of_ordered line 1351
  106. theorem OAI.Erdos3.FixedDensity.hasUniformCyclicPartiteSimplexRemoval_add_two_of_ordered line 1371
  107. theorem OAI.Erdos3.FixedDensity.exists_uniformDenseAPCount_of_orderedRemoval line 1388
  108. theorem OAI.Erdos3.FixedDensity.exists_uniformWeightedAPCount_of_orderedRemoval line 1400
  109. theorem OAI.Erdos3.FixedDensity.exists_uniformDenseAPCount_of_orderedRemoval_of_two_le line 1412
  110. theorem OAI.Erdos3.FixedDensity.exists_uniformWeightedAPCount_of_orderedRemoval_of_two_le line 1431