OAI/Combinatorics/UniformKServer/SideReferenceSchedule.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual persistent U schedule, including changes of dominant identity. It has no per-epoch additive charge, and its non-wholesale changes are paid by held-size variation plus the existing wholesale ledger.

  1. def OAI.UniformKServer.SideReferenceSchedule.reset line 19
  2. def OAI.UniformKServer.SideReferenceSchedule.side line 23
  3. def OAI.UniformKServer.SideReferenceSchedule.reference line 28
  4. def OAI.UniformKServer.SideReferenceSchedule.wholesale line 31
  5. def OAI.UniformKServer.SideReferenceSchedule.charge line 34
  6. theorem OAI.UniformKServer.SideReferenceSchedule.side_nonneg line 38
  7. theorem OAI.UniformKServer.SideReferenceSchedule.side_le_total line 45
  8. theorem OAI.UniformKServer.SideReferenceSchedule.not_reset_dominant line 54
  9. theorem OAI.UniformKServer.SideReferenceSchedule.side_difference line 64
  10. theorem OAI.UniformKServer.SideReferenceSchedule.reference_nonneg line 74
  11. theorem OAI.UniformKServer.SideReferenceSchedule.reference_compared line 78
  12. theorem OAI.UniformKServer.SideReferenceSchedule.reference_spec line 83
  13. theorem OAI.UniformKServer.SideReferenceSchedule.wholesale_budget line 94
  14. theorem OAI.UniformKServer.SideReferenceSchedule.charge_bound line 102
  15. theorem OAI.UniformKServer.SideReferenceSchedule.expenditure_bound line 125
  16. theorem OAI.UniformKServer.SideReferenceSchedule.budget line 138