OAI/Combinatorics/UniformKServer/TierSchedule.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal insertion schedule. It inspects chronological ages, not realized lifetimes, and is defined before any radius or lifetime tape.

  1. def OAI.UniformKServer.TierSchedule.trigger line 17
  2. def OAI.UniformKServer.TierSchedule.run line 20
  3. theorem OAI.UniformKServer.TierSchedule.index_lt line 26
  4. theorem OAI.UniformKServer.TierSchedule.increasing line 39
  5. theorem OAI.UniformKServer.TierSchedule.chronological_coverage line 47
  6. theorem OAI.UniformKServer.TierSchedule.young_next_subset line 63