OAI/Computability/BinPacking/Packing/PackingScalar.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.Role line 30
  2. instance OAI.BinPackingGap.(instance at line 38) line 38
  3. inductive OAI.BinPackingGap.Subclass line 42
  4. instance OAI.BinPackingGap.(instance at line 58) line 58
  5. inductive OAI.BinPackingGap.Pattern line 62
  6. instance OAI.BinPackingGap.(instance at line 69) line 69
  7. def OAI.BinPackingGap.Role.index line 75
  8. theorem OAI.BinPackingGap.Role.index_injective line 82
  9. theorem OAI.BinPackingGap.Role.sum_univ line 86
  10. def OAI.BinPackingGap.Subclass.role line 95
  11. theorem OAI.BinPackingGap.role_eq_x_iff line 102
  12. theorem OAI.BinPackingGap.role_eq_anchor_iff line 106
  13. theorem OAI.BinPackingGap.role_eq_global_iff line 110
  14. theorem OAI.BinPackingGap.role_eq_local_iff line 114
  15. theorem OAI.BinPackingGap.role_eq_flag_iff line 118
  16. def OAI.BinPackingGap.patternSubclass line 122
  17. theorem OAI.BinPackingGap.patternSubclass_role line 144
  18. theorem OAI.BinPackingGap.patternSubclass_injective line 148
  19. theorem OAI.BinPackingGap.patternSubclass_function_injective line 153
  20. theorem OAI.BinPackingGap.card_role line 159
  21. theorem OAI.BinPackingGap.card_subclass line 161
  22. theorem OAI.BinPackingGap.card_pattern line 163
  23. def OAI.BinPackingGap.IsPatternTuple line 165
  24. theorem OAI.BinPackingGap.existsUnique_role_of_pattern line 168
  25. theorem OAI.BinPackingGap.pattern_eq_of_tuple line 178
  26. def OAI.BinPackingGap.labelWeight line 196
  27. def OAI.BinPackingGap.labelSecondary line 198
  28. theorem OAI.BinPackingGap.labelWeight_pos line 201
  29. theorem OAI.BinPackingGap.labelWeight_le line 204
  30. theorem OAI.BinPackingGap.labelWeight_strictMono line 209
  31. theorem OAI.BinPackingGap.labelWeight_mono line 215
  32. theorem OAI.BinPackingGap.labelWeight_gap line 219
  33. theorem OAI.BinPackingGap.labelSecondary_nonpos_bounds line 231
  34. theorem OAI.BinPackingGap.labelSecondary_nonpos_iff line 245
  35. theorem OAI.BinPackingGap.labelSecondary_self line 255
  36. theorem OAI.BinPackingGap.labelSecondary_eq_zero_iff line 260
  37. def OAI.BinPackingGap.subclassIndicator line 282
  38. def OAI.BinPackingGap.primaryCoeff line 284
  39. def OAI.BinPackingGap.primaryScore line 299
  40. def OAI.BinPackingGap.primaryBound line 302
  41. def OAI.BinPackingGap.roleCoeffIndex line 304
  42. theorem OAI.BinPackingGap.primaryCoeff_role line 307
  43. theorem OAI.BinPackingGap.primaryCoeff_abs_le line 311
  44. theorem OAI.BinPackingGap.primaryScore_abs_lt line 315
  45. theorem OAI.BinPackingGap.sum_primaryScore_eq line 321
  46. def OAI.BinPackingGap.roleCount line 327
  47. def OAI.BinPackingGap.subclassCount line 330
  48. theorem OAI.BinPackingGap.sum_primaryCoeff_role line 333
  49. theorem OAI.BinPackingGap.sum_primaryCoeff_five line 340
  50. theorem OAI.BinPackingGap.sum_primaryCoeff_six line 345
  51. theorem OAI.BinPackingGap.sum_primaryCoeff_seven line 350
  52. theorem OAI.BinPackingGap.sum_primaryCoeff_eight line 356
  53. theorem OAI.BinPackingGap.sum_primaryCoeff_nine line 361
  54. theorem OAI.BinPackingGap.radix100_eq_zero_iff line 365
  55. theorem OAI.BinPackingGap.primaryCoeff_total_abs_lt line 395
  56. theorem OAI.BinPackingGap.sum_primaryScore_eq_zero_iff_coefficients line 404
  57. theorem OAI.BinPackingGap.pattern_primaryCoeff_sum line 409
  58. theorem OAI.BinPackingGap.sum_role_subclassIndicator line 415
  59. theorem OAI.BinPackingGap.roleTuple_eq_pattern line 428
  60. theorem OAI.BinPackingGap.sum_primaryScore_eq_zero_iff_pattern line 471
  61. theorem OAI.BinPackingGap.sum_primaryScore_eq_zero_of_coefficients line 513
  62. def OAI.BinPackingGap.secondaryScore line 523
  63. theorem OAI.BinPackingGap.secondaryScore_none line 532
  64. def OAI.BinPackingGap.tableRoleLabel line 536
  65. def OAI.BinPackingGap.gamma line 543
  66. def OAI.BinPackingGap.mu line 545
  67. def OAI.BinPackingGap.nu line 547
  68. def OAI.BinPackingGap.encodedSize line 549
  69. theorem OAI.BinPackingGap.gamma_pos line 553
  70. theorem OAI.BinPackingGap.gamma_le_one line 556
  71. theorem OAI.BinPackingGap.gamma_mul_primaryBound line 559
  72. theorem OAI.BinPackingGap.mu_pos line 562
  73. theorem OAI.BinPackingGap.nu_pos line 565
  74. theorem OAI.BinPackingGap.mu_mul_labelBound line 567
  75. theorem OAI.BinPackingGap.mu_le_gamma_div line 572
  76. theorem OAI.BinPackingGap.nu_le_gamma_div line 578
  77. theorem OAI.BinPackingGap.secondaryScore_abs_le line 582
  78. theorem OAI.BinPackingGap.secondaryScore_rat_abs_le line 593
  79. theorem OAI.BinPackingGap.primaryScore_rat_abs_le line 597
  80. theorem OAI.BinPackingGap.perturbation_triangle line 601
  81. theorem OAI.BinPackingGap.perturbation_small line 619
  82. theorem OAI.BinPackingGap.encodedSize_perturbation_bound line 627
  83. theorem OAI.BinPackingGap.encodedSize_mem_interval line 644
  84. theorem OAI.BinPackingGap.primary_tail_lt line 650
  85. theorem OAI.BinPackingGap.secondary_tail_lt line 660
  86. def OAI.BinPackingGap.Packing.primaryTotal line 671
  87. def OAI.BinPackingGap.Packing.IsTableBin line 674
  88. abbrev OAI.BinPackingGap.Packing.TableBin line 677
  89. instance OAI.BinPackingGap.Packing.(instance at line 680) line 680
  90. instance OAI.BinPackingGap.Packing.(instance at line 683) line 683
  91. theorem OAI.BinPackingGap.Packing.table_pattern line 686
  92. def OAI.BinPackingGap.Packing.tablePattern line 704
  93. def OAI.BinPackingGap.Packing.tableEquiv line 708
  94. theorem OAI.BinPackingGap.Packing.tableEquiv_subclass line 712
  95. def OAI.BinPackingGap.Packing.itemAtRole line 718
  96. theorem OAI.BinPackingGap.Packing.itemAtRole_mem line 722
  97. theorem OAI.BinPackingGap.Packing.itemAtRole_subclass line 727
  98. theorem OAI.BinPackingGap.Packing.itemAtRole_role line 733
  99. theorem OAI.BinPackingGap.Packing.itemAtRole_injective line 738
  100. theorem OAI.BinPackingGap.Packing.itemAtRole_joint_injective line 743
  101. theorem OAI.BinPackingGap.Packing.mem_table_bin_iff line 755
  102. theorem OAI.BinPackingGap.Packing.itemAtRole_eq_of_mem line 765
  103. def OAI.BinPackingGap.Packing.IsGoodTableBin line 775
  104. abbrev OAI.BinPackingGap.Packing.GoodTableBin line 781
  105. instance OAI.BinPackingGap.Packing.(instance at line 785) line 785
  106. abbrev OAI.BinPackingGap.Packing.GoodM line 789
  107. abbrev OAI.BinPackingGap.Packing.GoodG line 793
  108. instance OAI.BinPackingGap.Packing.(instance at line 797) line 797
  109. instance OAI.BinPackingGap.Packing.(instance at line 801) line 801
  110. def OAI.BinPackingGap.primaryTotal line 811
  111. def OAI.BinPackingGap.secondaryTotal line 813
  112. def OAI.BinPackingGap.coordinateTotal line 816
  113. theorem OAI.BinPackingGap.encodedSize_sum line 818
  114. theorem OAI.BinPackingGap.secondaryTotal_rat_abs_le line 826
  115. theorem OAI.BinPackingGap.coordinateTotal_abs_le line 837
  116. theorem OAI.BinPackingGap.sum_primary_nonpos_of_feasible line 844
  117. theorem OAI.BinPackingGap.sum_secondary_nonpos_of_feasible line 862
  118. theorem OAI.BinPackingGap.feasible_iff_coordinateSum_nonpos line 879
  119. theorem OAI.BinPackingGap.secondaryTotal_eq_labelSecondary line 893
  120. theorem OAI.BinPackingGap.secondaryTotal_nonpos_iff_labels line 916
  121. theorem OAI.BinPackingGap.secondaryTotal_eq_zero_iff_labels line 924
  122. def OAI.BinPackingGap.Packing.fiveEquiv line 936
  123. theorem OAI.BinPackingGap.Packing.sum_fiveEquiv line 939
  124. theorem OAI.BinPackingGap.Packing.full_primary_nonpos line 946
  125. theorem OAI.BinPackingGap.Packing.table_secondary_nonpos line 966
  126. theorem OAI.BinPackingGap.Packing.sum_itemAtRole line 993
  127. theorem OAI.BinPackingGap.Packing.table_secondary_eq line 1002
  128. theorem OAI.BinPackingGap.Packing.table_labels_le_anchor line 1014
  129. theorem OAI.BinPackingGap.Packing.table_coordinate_nonpos line 1026
  130. theorem OAI.BinPackingGap.Packing.table_coordinate_nonpos_of_same_label line 1059
  131. def OAI.BinPackingGap.Packing.outsideTableItems line 1072
  132. theorem OAI.BinPackingGap.Packing.outsideTableItems_card_lt line 1077