OAI/Computability/BinPacking/Inventory/CurrentMatches.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.CoverageCounts.interval_prefix_card line 22
  2. theorem OAI.BinPackingGap.CoverageCounts.ordered_short_long_partition line 50
  3. theorem OAI.BinPackingGap.CoverageCounts.card_le_good_card_add line 74
  4. theorem OAI.BinPackingGap.CoverageCounts.card_le_target_add_loss line 82
  5. theorem OAI.BinPackingGap.CoverageCounts.card_add_card_le_of_disjoint_injections line 91
  6. theorem OAI.BinPackingGap.CoverageCounts.card_three_le_of_disjoint_injections line 100
  7. theorem OAI.BinPackingGap.CoverageCounts.card_le_add_of_subset_union line 116
  8. theorem OAI.BinPackingGap.CoverageCounts.displaced_baseline_bound line 122
  9. theorem OAI.BinPackingGap.CoverageCounts.coverage_lower_bound line 128
  10. theorem OAI.BinPackingGap.CoverageCounts.displaced_short_correction line 133
  11. theorem OAI.BinPackingGap.CoverageCounts.short_le_displaced_add_long line 139
  12. theorem OAI.BinPackingGap.CoverageCounts.long_match_lower_bound line 145
  13. def OAI.BinPackingGap.IntervalCoverage.prefixSet line 158
  14. def OAI.BinPackingGap.IntervalCoverage.prefixCount line 162
  15. def OAI.BinPackingGap.IntervalCoverage.coverageSet line 164
  16. def OAI.BinPackingGap.IntervalCoverage.coverageCount line 168
  17. theorem OAI.BinPackingGap.IntervalCoverage.mem_prefixSet line 171
  18. theorem OAI.BinPackingGap.IntervalCoverage.mem_coverageSet line 176
  19. theorem OAI.BinPackingGap.IntervalCoverage.completion_prefix_identity line 181
  20. structure OAI.BinPackingGap.IntervalCoverage.ShiftData line 188
  21. def OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline line 203
  22. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline_designated line 208
  23. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline_undesignated line 215
  24. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.designated_block_card line 223
  25. def OAI.BinPackingGap.IntervalCoverage.ShiftData.activeTests line 231
  26. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.mem_activeTests line 235
  27. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline_prefix_of_agrees line 240
  28. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline_prefix line 275
  29. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.activeTests_card line 279
  30. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline_prefix_disjoint_of_agrees line 300
  31. theorem OAI.BinPackingGap.IntervalCoverage.ShiftData.deadline_prefix_disjoint line 311
  32. theorem OAI.BinPackingGap.IntervalCoverage.exists_equiv_of_prefix_dominance line 322
  33. def OAI.BinPackingGap.Coverage.goodTuplesAt line 377
  34. def OAI.BinPackingGap.Coverage.mainTuplesAt line 383
  35. def OAI.BinPackingGap.Coverage.edgeTuplesAt line 388
  36. theorem OAI.BinPackingGap.Coverage.mem_goodTuplesAt line 393
  37. theorem OAI.BinPackingGap.Coverage.mem_mainTuplesAt line 400
  38. theorem OAI.BinPackingGap.Coverage.mem_edgeTuplesAt line 408
  39. theorem OAI.BinPackingGap.Coverage.mainTuplesAt_subset_good line 416
  40. theorem OAI.BinPackingGap.Coverage.edgeTuplesAt_subset_good line 422
  41. theorem OAI.BinPackingGap.Coverage.goodTuplesAt_eq_union line 428
  42. theorem OAI.BinPackingGap.Coverage.mainTuplesAt_disjoint_edge line 437
  43. theorem OAI.BinPackingGap.Coverage.goodTuplesAt_disjoint_label line 445
  44. theorem OAI.BinPackingGap.Coverage.mainTuplesAt_disjoint_label line 454
  45. theorem OAI.BinPackingGap.Coverage.edgeTuplesAt_disjoint_label line 460
  46. def OAI.BinPackingGap.Coverage.roleItems line 466
  47. theorem OAI.BinPackingGap.Coverage.roleItems_card line 470
  48. def OAI.BinPackingGap.Coverage.anchorItemsAt line 474
  49. theorem OAI.BinPackingGap.Coverage.mem_anchorItemsAt line 479
  50. def OAI.BinPackingGap.Coverage.badAnchorsAt line 486
  51. theorem OAI.BinPackingGap.Coverage.mem_badAnchorsAt line 491
  52. theorem OAI.BinPackingGap.Coverage.good_anchorItems_subset line 498
  53. theorem OAI.BinPackingGap.Coverage.card_le_role_resources line 507
  54. theorem OAI.BinPackingGap.Coverage.card_three_le_row_resources line 513
  55. def OAI.BinPackingGap.Coverage.tupleCompletion line 522
  56. theorem OAI.BinPackingGap.Coverage.tupleCompletion_le_baseline line 529
  57. def OAI.BinPackingGap.Coverage.baselinePrefixAt line 538
  58. def OAI.BinPackingGap.Coverage.completionPrefixAt line 543
  59. def OAI.BinPackingGap.Coverage.coveringTuplesAt line 548
  60. theorem OAI.BinPackingGap.Coverage.completion_prefix_decomposition line 555
  61. theorem OAI.BinPackingGap.Coverage.literal_completion_prefix_decomposition line 566
  62. def OAI.BinPackingGap.Coverage.deadlinePrefixAt line 582
  63. theorem OAI.BinPackingGap.Coverage.mem_deadlinePrefixAt line 588
  64. theorem OAI.BinPackingGap.Coverage.good_deadline_subset_completed_anchor_image line 596
  65. theorem OAI.BinPackingGap.Coverage.deadline_prefix_le_completion_add_loss line 634
  66. def OAI.BinPackingGap.Coverage.jobRowPrefixAt line 650
  67. def OAI.BinPackingGap.Coverage.treeRowPrefixAt line 656
  68. def OAI.BinPackingGap.Coverage.keyPrefixAt line 663
  69. def OAI.BinPackingGap.Coverage.edgePrefixAt line 669
  70. def OAI.BinPackingGap.Coverage.mainJobPrefixAt line 674
  71. def OAI.BinPackingGap.Coverage.mainTreePrefixAt line 681
  72. theorem OAI.BinPackingGap.Coverage.baseline_prefix_row_partition line 688
  73. theorem OAI.BinPackingGap.Coverage.main_tree_prefix_le_inventory line 700
  74. theorem OAI.BinPackingGap.Coverage.good_key_subset_edge_anchor_image line 721
  75. theorem OAI.BinPackingGap.Coverage.key_prefix_le_edge_prefix_add_loss line 748
  76. theorem OAI.BinPackingGap.Coverage.edge_row_mem_job_prefix line 762
  77. theorem OAI.BinPackingGap.Coverage.displaced_baseline_prefix_le line 774
  78. def OAI.BinPackingGap.Coverage.currentKeyItemsAt line 828
  79. def OAI.BinPackingGap.Coverage.currentEdgeTuplesAt line 835
  80. def OAI.BinPackingGap.Coverage.displacedTuplesAt line 841
  81. def OAI.BinPackingGap.Coverage.currentShortMainAt line 847
  82. def OAI.BinPackingGap.Coverage.currentShortEdgeAt line 854
  83. def OAI.BinPackingGap.Coverage.currentLongEdgeAt line 861
  84. def OAI.BinPackingGap.Coverage.currentShortItemsAt line 868
  85. theorem OAI.BinPackingGap.Coverage.key_subset_le_matching_add_loss line 875
  86. theorem OAI.BinPackingGap.Coverage.current_key_count_le_matches_add_loss line 909
  87. theorem OAI.BinPackingGap.Coverage.current_match_partition line 923
  88. theorem OAI.BinPackingGap.Coverage.current_short_consumption_le_stock line 941
  89. theorem OAI.BinPackingGap.Coverage.current_long_matches_from_correction line 973