OAI/Combinatorics/KServer/OutputRules.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Rule I applied to the actual scheduled proportions and caps. Its only external numeric input is a parent allocation covering the sum of the child lower envelopes at the parent's parameter (the rank superadditivity premise).

  1. lemma OAI.KServer.ActualOutput.inactive_flexcap line 14
  2. lemma OAI.KServer.ActualOutput.regular_upper line 23
  3. lemma OAI.KServer.ActualOutput.own_flex_le line 29
  4. lemma OAI.KServer.ActualOutput.cap_lower line 38
  5. lemma OAI.KServer.ActualOutput.error_sum line 48
  6. lemma OAI.KServer.ActualOutput.dominant_slack line 65
  7. def OAI.KServer.ActualOutput.outI line 97
  8. lemma OAI.KServer.ActualOutput.ruleI_T line 100
  9. lemma OAI.KServer.ActualOutput.outI_feasible line 107
  10. def OAI.KServer.ActualOutput.sides line 190
  11. def OAI.KServer.ActualOutput.sideData line 191
  12. def OAI.KServer.ActualOutput.side line 193
  13. def OAI.KServer.ActualOutput.slack line 195
  14. lemma OAI.KServer.ActualOutput.sides_eq line 198
  15. lemma OAI.KServer.ActualOutput.side_mem line 202
  16. lemma OAI.KServer.ActualOutput.side_core line 205
  17. lemma OAI.KServer.ActualOutput.side_core_total line 215
  18. lemma OAI.KServer.ActualOutput.side_logs line 223
  19. lemma OAI.KServer.ActualOutput.side_upper line 227
  20. lemma OAI.KServer.ActualOutput.side_lower line 244
  21. lemma OAI.KServer.ActualOutput.slack_nonneg line 278
  22. lemma OAI.KServer.ActualOutput.slack_exp line 284
  23. lemma OAI.KServer.ActualOutput.slack_sum line 295
  24. lemma OAI.KServer.ActualOutput.side_slack_paid line 321
  25. def OAI.KServer.ActualOutput.sideOut line 346
  26. def OAI.KServer.ActualOutput.outII line 348
  27. lemma OAI.KServer.ActualOutput.sideOut_feasible line 351
  28. lemma OAI.KServer.ActualOutput.sideOut_parent line 367
  29. lemma OAI.KServer.ActualOutput.outII_feasible line 386
  30. def OAI.KServer.RuleSchedule.choose line 446

    Source documentation

    true is rule II. Ties select I at a restart.

    def choose (S D : ℝ) : Bool := decide (S < D/2)

    Mentions: OAI.KServer.RuleSchedule.S

  31. def OAI.KServer.RuleSchedule.update line 447
  32. def OAI.KServer.RuleSchedule.step line 449
  33. def OAI.KServer.RuleSchedule.run line 452
  34. def OAI.KServer.RuleSchedule.allowed line 457
  35. lemma OAI.KServer.RuleSchedule.choose_allowed line 461
  36. lemma OAI.KServer.RuleSchedule.step_allowed line 470
  37. lemma OAI.KServer.RuleSchedule.run_allowed line 490
  38. def OAI.KServer.RuleSchedule.value line 495
  39. def OAI.KServer.RuleSchedule.charge line 498
  40. lemma OAI.KServer.RuleSchedule.value_nonneg line 503
  41. lemma OAI.KServer.RuleSchedule.value_upper line 506
  42. lemma OAI.KServer.RuleSchedule.charge_nonneg line 509
  43. lemma OAI.KServer.RuleSchedule.ordinary_credit line 514
  44. def OAI.KServer.RuleSchedule.core line 535
  45. def OAI.KServer.RuleSchedule.coefficient line 537
  46. lemma OAI.KServer.RuleSchedule.input_difference line 541
  47. lemma OAI.KServer.RuleSchedule.core_nonneg line 550
  48. lemma OAI.KServer.RuleSchedule.input_lipschitz line 554
  49. lemma OAI.KServer.RuleSchedule.data_change line 564
  50. lemma OAI.KServer.RuleSchedule.run_congr line 578
  51. def OAI.KServer.ActualOutput.marked line 606
  52. def OAI.KServer.ActualOutput.reset line 608
  53. def OAI.KServer.ActualOutput.rule line 611
  54. def OAI.KServer.ActualOutput.out line 613
  55. lemma OAI.KServer.ActualOutput.rule_allowed line 619
  56. lemma OAI.KServer.ActualOutput.out_feasible line 622
  57. lemma OAI.KServer.ActualOutput.output_domination line 646