OAI/Combinatorics/KServer/AllocationBudget.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

True-prefix filtering followed by paid literal profile edits. In particular no event chosen at the new history is allowed to select a filtering term.

  1. lemma OAI.KServer.ScheduledFiltering.filtering_zero line 18
  2. lemma OAI.KServer.ScheduledFiltering.payment_step line 42
  3. lemma OAI.KServer.ScheduledFiltering.payment line 85
  4. lemma OAI.KServer.ScheduledFiltering.bounded_endpoint line 111
  5. lemma OAI.KServer.SideFiltering.filtering_zero line 153
  6. lemma OAI.KServer.SideFiltering.slope line 178
  7. lemma OAI.KServer.SideFiltering.payment_step line 195
  8. lemma OAI.KServer.SideFiltering.payment line 241
  9. lemma OAI.KServer.ActualCharges.drift_le_stock line 285
  10. lemma OAI.KServer.ActualCharges.raw_drift_eq line 288
  11. lemma OAI.KServer.ActualCharges.simplex_mass line 292
  12. lemma OAI.KServer.ActualCharges.simplex_movement line 298
  13. lemma OAI.KServer.ActualCharges.side_endpoint line 324
  14. lemma OAI.KServer.ActualCharges.side_movement line 351
  15. def OAI.KServer.ActualCharges.ruleConstant line 394
  16. lemma OAI.KServer.ActualCharges.ruleConstant_nonneg line 395
  17. lemma OAI.KServer.ActualCharges.core_coarse line 401
  18. lemma OAI.KServer.ActualCharges.joint_coarse line 407
  19. lemma OAI.KServer.ActualCharges.ruleS_eq line 412
  20. lemma OAI.KServer.ActualCharges.ruleJ_eq line 414
  21. lemma OAI.KServer.ActualCharges.rule_expense_step line 418
  22. lemma OAI.KServer.ActualCharges.rule_expense line 441
  23. lemma OAI.KServer.ActualCharges.rule_initial line 452
  24. lemma OAI.KServer.ActualCharges.switch_movement line 467
  25. lemma OAI.KServer.ActualOutput.coarse_output line 500
  26. lemma OAI.KServer.ActualOutput.wholesale_output line 518
  27. lemma OAI.KServer.ActualOutput.all_movement line 539
  28. def OAI.KServer.ActualCharges.fineConstant line 576
  29. def OAI.KServer.ActualCharges.movementConstant line 577
  30. def OAI.KServer.ActualCharges.endpointConstant line 579
  31. def OAI.KServer.ActualCharges.localConstant line 580
  32. lemma OAI.KServer.ActualCharges.output_constants_nonneg line 581
  33. lemma OAI.KServer.ActualCharges.fine_movement line 597
  34. lemma OAI.KServer.ActualCharges.output_movement line 616
  35. lemma OAI.KServer.ActualCharges.local_movement line 646
  36. lemma OAI.KServer.HierarchicalQuota.sum_snoc line 683
  37. lemma OAI.KServer.HierarchicalQuota.total_sum line 689
  38. lemma OAI.KServer.HierarchicalQuota.drift_flat line 695
  39. def OAI.KServer.HierarchicalQuota.nodeMove line 705
  40. def OAI.KServer.HierarchicalQuota.levelMove line 707
  41. def OAI.KServer.HierarchicalQuota.levelDrift line 708
  42. def OAI.KServer.HierarchicalQuota.levelInventory line 710
  43. lemma OAI.KServer.HierarchicalQuota.levelMove_nonneg line 713
  44. lemma OAI.KServer.HierarchicalQuota.levelDrift_nonneg line 716
  45. lemma OAI.KServer.HierarchicalQuota.levelMove_zero line 719
  46. lemma OAI.KServer.HierarchicalQuota.levelDrift_zero line 721
  47. lemma OAI.KServer.HierarchicalQuota.level_movement line 744
  48. lemma OAI.KServer.HierarchicalQuota.weighted_shift line 776
  49. def OAI.KServer.HierarchicalQuota.treeMove line 801
  50. def OAI.KServer.HierarchicalQuota.treeDrift line 803
  51. def OAI.KServer.HierarchicalQuota.treeInventory line 805
  52. lemma OAI.KServer.HierarchicalQuota.treeInventory_nonneg line 807
  53. theorem OAI.KServer.HierarchicalQuota.allocation_absorption line 812
  54. lemma OAI.KServer.HierarchicalQuota.histogram_distance line 851
  55. def OAI.KServer.HierarchicalQuota.address line 882
  56. def OAI.KServer.HierarchicalQuota.prefixCross line 883
  57. def OAI.KServer.HierarchicalQuota.levelHidden line 886
  58. lemma OAI.KServer.HierarchicalQuota.count_histogram line 890
  59. lemma OAI.KServer.HierarchicalQuota.level_drift_count line 899
  60. lemma OAI.KServer.HierarchicalQuota.level_count_cross line 912
  61. lemma OAI.KServer.HierarchicalQuota.prefixCross_nonneg line 922