OAI/Combinatorics/UniformKServer/StarAllocator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The actual causal star allocator. At time zero it uses the true lower requirements, avoiding an unjustified feasibility claim for the arbitrary initial minimizer states. All subsequent outputs are the source's two rules.

  1. theorem OAI.UniformKServer.StarAllocator.wholesale_measurable line 19
  2. def OAI.UniformKServer.StarAllocator.switchData line 27
  3. def OAI.UniformKServer.StarAllocator.tag line 35
  4. def OAI.UniformKServer.StarAllocator.ruleOutput line 38
  5. def OAI.UniformKServer.StarAllocator.output line 45
  6. theorem OAI.UniformKServer.StarAllocator.tag_valid line 50
  7. theorem OAI.UniformKServer.StarAllocator.rule_lower line 54
  8. theorem OAI.UniformKServer.StarAllocator.rule_upper line 69
  9. theorem OAI.UniformKServer.StarAllocator.rule_budget line 78
  10. theorem OAI.UniformKServer.StarAllocator.lower_mono line 87
  11. theorem OAI.UniformKServer.StarAllocator.lower_cap line 93
  12. theorem OAI.UniformKServer.StarAllocator.feasible line 103
  13. theorem OAI.UniformKServer.StarAllocator.nonneg line 114
  14. theorem OAI.UniformKServer.StarAllocator.cap_measurable line 118
  15. theorem OAI.UniformKServer.StarAllocator.childBeta_measurable line 125
  16. theorem OAI.UniformKServer.StarAllocator.lower_measurable line 131
  17. theorem OAI.UniformKServer.StarAllocator.rule_measurable line 140
  18. theorem OAI.UniformKServer.StarAllocator.measurable line 149