OAI/Combinatorics/UniformKServer/AllocationSchedule.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Exact coarse held-size schedule in companion §03. The deterministic potential below pays relative refreshes and both hysteretic on/off transitions from variation of the underlying persistent rank estimates. In particular it does not restart any initialization allowance when a child becomes active.

  1. def OAI.UniformKServer.AllocationSchedule.compared line 16
  2. def OAI.UniformKServer.AllocationSchedule.relativeUpdate line 18
  3. def OAI.UniformKServer.AllocationSchedule.size line 22
  4. def OAI.UniformKServer.AllocationSchedule.update line 26
  5. def OAI.UniformKServer.AllocationSchedule.charge line 31
  6. def OAI.UniformKServer.AllocationSchedule.potential line 33
  7. theorem OAI.UniformKServer.AllocationSchedule.charge_self line 36
  8. theorem OAI.UniformKServer.AllocationSchedule.charge_le line 38
  9. theorem OAI.UniformKServer.AllocationSchedule.failure_cost line 44
  10. theorem OAI.UniformKServer.AllocationSchedule.relative_nonneg line 65
  11. theorem OAI.UniformKServer.AllocationSchedule.relative_compared line 68
  12. theorem OAI.UniformKServer.AllocationSchedule.relative_drop line 75
  13. theorem OAI.UniformKServer.AllocationSchedule.update_nonneg line 85
  14. theorem OAI.UniformKServer.AllocationSchedule.potential_nonneg line 99
  15. theorem OAI.UniformKServer.AllocationSchedule.update_drop line 103
  16. theorem OAI.UniformKServer.AllocationSchedule.potential_change line 134
  17. theorem OAI.UniformKServer.AllocationSchedule.update_step line 144
  18. def OAI.UniformKServer.AllocationSchedule.schedule line 151
  19. theorem OAI.UniformKServer.AllocationSchedule.schedule_nonneg line 155
  20. theorem OAI.UniformKServer.AllocationSchedule.schedule_budget line 162
  21. def OAI.UniformKServer.AllocationSchedule.held line 185

    Source documentation

    A single relative-held reference, used for the parent and for one side epoch.

    def held (δ : ℝ) (x : ℕ → ℝ) : ℕ → ℝ
  | 0 => x 0
  | t+1 => relativeUpdate δ (held δ x t) (x (t+1))

    Mentions: OAI.UniformKServer.AllocationSchedule.relativeUpdate

  22. theorem OAI.UniformKServer.AllocationSchedule.held_nonneg line 189
  23. theorem OAI.UniformKServer.AllocationSchedule.held_compared line 196
  24. theorem OAI.UniformKServer.AllocationSchedule.relative_step line 202
  25. theorem OAI.UniformKServer.AllocationSchedule.held_budget line 213
  26. theorem OAI.UniformKServer.AllocationSchedule.update_inactive line 232
  27. theorem OAI.UniformKServer.AllocationSchedule.update_active line 247
  28. theorem OAI.UniformKServer.AllocationSchedule.initial_potential_bound line 268
  29. theorem OAI.UniformKServer.AllocationSchedule.side_charge line 278

    Source documentation

    Side charge uses actual totals, not the held values.

    theorem side_charge {δ b x y : ℝ} (hδ : 0 ≤ δ) (hy : 0 ≤ y)
    (hcmp : compared δ b x) : x+y ≤ (1+δ)*(b+y) := by
…

    Mentions: OAI.UniformKServer.AllocationSchedule.compared