OAI/Combinatorics/UniformKServer/TierShortSchedule.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Deterministic expected short-roster functions on the actual chronological insertion records. These auxiliary experiments never select actual keys.

  1. def OAI.UniformKServer.TierShortSchedule.run line 18
  2. theorem OAI.UniformKServer.TierShortSchedule.valid line 28
  3. def OAI.UniformKServer.TierShortSchedule.parameter line 47
  4. theorem OAI.UniformKServer.TierShortSchedule.insertion_payment line 51