OAI/Combinatorics/KServer/ScheduleBudget.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

Exact structural identifications of the scheduled integral family and bounds on the actual slack coefficients.

  1. lemma OAI.KServer.ScheduleShape.eta_bound line 19
  2. lemma OAI.KServer.ScheduleShape.regular_data line 36
  3. lemma OAI.KServer.ScheduleShape.marked_data line 49
  4. lemma OAI.KServer.ScheduledPayment.ordinary_regular line 81
  5. lemma OAI.KServer.ScheduledPayment.ordinary_marked line 156
  6. def OAI.KServer.SingletonPayment.point line 262
  7. lemma OAI.KServer.SingletonPayment.point_mem line 264
  8. lemma OAI.KServer.SingletonPayment.singleton_eq line 271
  9. lemma OAI.KServer.SingletonPayment.zero_value line 280
  10. lemma OAI.KServer.SingletonPayment.base_value line 284
  11. lemma OAI.KServer.SingletonPayment.core_value_bound line 288
  12. lemma OAI.KServer.SingletonPayment.candidate_singleton line 304
  13. lemma OAI.KServer.SingletonPayment.old_singleton line 314
  14. lemma OAI.KServer.SingletonPayment.marked_point_potential line 388
  15. lemma OAI.KServer.SingletonPayment.new_singleton line 393
  16. lemma OAI.KServer.ScheduledPayment.marked_zero_flag line 468
  17. lemma OAI.KServer.ScheduledPayment.marked_point_value line 480
  18. lemma OAI.KServer.ScheduledPayment.ordinary_old_zero line 493
  19. lemma OAI.KServer.ScheduledPayment.ordinary_new_zero line 555
  20. lemma OAI.KServer.ScheduledPayment.empty_total line 642
  21. lemma OAI.KServer.ScheduledPayment.positive_active line 650
  22. lemma OAI.KServer.ScheduledPayment.ordinary_nonempty line 656
  23. lemma OAI.KServer.ScheduledPayment.flags_nonneg line 673
  24. lemma OAI.KServer.ScheduledPayment.side_charge_nonneg line 681
  25. def OAI.KServer.ScheduledPayment.expense line 688
  26. lemma OAI.KServer.ScheduledPayment.expense_nonneg line 697
  27. lemma OAI.KServer.ScheduledPayment.mass_bound line 713
  28. lemma OAI.KServer.ScheduledPayment.wholesale_payment line 722
  29. lemma OAI.KServer.ScheduledPayment.expense_lower line 773
  30. lemma OAI.KServer.ScheduledPayment.payment line 788
  31. def OAI.KServer.ActualCharges.drift line 875
  32. def OAI.KServer.ActualCharges.inventory line 877
  33. def OAI.KServer.ActualCharges.flat line 878
  34. def OAI.KServer.ActualCharges.flags line 880
  35. def OAI.KServer.ActualCharges.active line 882
  36. def OAI.KServer.ActualCharges.parentCharge line 885
  37. def OAI.KServer.ActualCharges.wholesale line 887
  38. def OAI.KServer.ActualCharges.sideRefresh line 890
  39. def OAI.KServer.ActualCharges.activeConstant line 894
  40. def OAI.KServer.ActualCharges.parentConstant line 895
  41. def OAI.KServer.ActualCharges.flagConstant line 896
  42. lemma OAI.KServer.ActualCharges.constants_nonneg line 898
  43. lemma OAI.KServer.ActualCharges.inventory_nonneg line 900
  44. lemma OAI.KServer.ActualCharges.flags_nonneg line 905
  45. lemma OAI.KServer.ActualCharges.active_nonneg line 907
  46. lemma OAI.KServer.ActualCharges.parent_nonneg line 911
  47. lemma OAI.KServer.ActualCharges.wholesale_nonneg line 917
  48. lemma OAI.KServer.ActualCharges.sideRefresh_nonneg line 923
  49. lemma OAI.KServer.ActualCharges.flags_eq line 926
  50. lemma OAI.KServer.ActualCharges.flags_budget line 939
  51. lemma OAI.KServer.ActualCharges.inventory_flat line 945
  52. lemma OAI.KServer.ActualCharges.active_budget line 951
  53. lemma OAI.KServer.ActualCharges.parent_budget line 976
  54. lemma OAI.KServer.ActualCharges.wholesale_budget line 984
  55. lemma OAI.KServer.ActualCharges.sideRefresh_budget line 991
  56. def OAI.KServer.ActualCharges.total line 1012
  57. def OAI.KServer.ActualCharges.stock line 1013
  58. def OAI.KServer.ActualCharges.wholesaleConstant line 1016
  59. def OAI.KServer.ActualCharges.scaleConstant line 1017
  60. def OAI.KServer.ActualCharges.sideRefreshConstant line 1018
  61. lemma OAI.KServer.ActualCharges.total_mono line 1020
  62. lemma OAI.KServer.ActualCharges.total_nonneg line 1022
  63. lemma OAI.KServer.ActualCharges.total_add line 1024
  64. lemma OAI.KServer.ActualCharges.total_mul line 1027
  65. lemma OAI.KServer.ActualCharges.stock_nonneg line 1030
  66. lemma OAI.KServer.ActualCharges.inventory_child_le line 1032
  67. lemma OAI.KServer.ActualCharges.inventory_parent_le line 1034
  68. lemma OAI.KServer.ActualCharges.more_constants_nonneg line 1036
  69. lemma OAI.KServer.ActualCharges.flags_bound line 1045
  70. lemma OAI.KServer.ActualCharges.active_bound line 1048
  71. lemma OAI.KServer.ActualCharges.parent_bound line 1051
  72. lemma OAI.KServer.ActualCharges.wholesale_bound line 1054
  73. lemma OAI.KServer.ActualCharges.sideRefresh_bound line 1064
  74. lemma OAI.KServer.ActualCharges.scale_eq line 1072
  75. lemma OAI.KServer.ActualCharges.scale_bound line 1078
  76. lemma OAI.KServer.SidePayment.pre_actual line 1119
  77. lemma OAI.KServer.SidePayment.post_actual line 1146
  78. lemma OAI.KServer.SideFixed.payment line 1189
  79. lemma OAI.KServer.SideFixed.payment_of_edits line 1206
  80. lemma OAI.KServer.SidePayment.ordinary line 1241
  81. lemma OAI.KServer.SideActualBounds.scale_bound line 1293
  82. lemma OAI.KServer.SideActualBounds.core_bound line 1305
  83. lemma OAI.KServer.SideActualBounds.endpoint line 1323
  84. lemma OAI.KServer.SideActualBounds.variation_bound line 1355
  85. def OAI.KServer.SidePayment.expense line 1378
  86. lemma OAI.KServer.SidePayment.payment line 1386
  87. def OAI.KServer.ActualCharges.simplexConstant line 1444
  88. def OAI.KServer.ActualCharges.sideConstant line 1446
  89. lemma OAI.KServer.ActualCharges.edit_constants_nonneg line 1448
  90. lemma OAI.KServer.ActualCharges.simplex_expense line 1457
  91. lemma OAI.KServer.ActualCharges.side_expense_step line 1483
  92. lemma OAI.KServer.ActualCharges.side_expense line 1511