OAI/Combinatorics/UniformKServer/HeldRelative.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Held scalar references with forced epoch resets. The potential is not restarted: its nonnegative value is discarded on a wholesale step, while the full new installation is charged to that step.

  1. def OAI.UniformKServer.HeldRelative.update line 17
  2. def OAI.UniformKServer.HeldRelative.schedule line 20
  3. theorem OAI.UniformKServer.HeldRelative.update_nonneg line 24
  4. theorem OAI.UniformKServer.HeldRelative.update_compared line 30
  5. theorem OAI.UniformKServer.HeldRelative.schedule_nonneg line 37
  6. theorem OAI.UniformKServer.HeldRelative.schedule_compared line 44
  7. def OAI.UniformKServer.HeldRelative.expenditure line 54
  8. theorem OAI.UniformKServer.HeldRelative.step line 57
  9. theorem OAI.UniformKServer.HeldRelative.budget line 74
  10. theorem OAI.UniformKServer.HeldRelative.true_charge line 101

    Source documentation

    The source charges true side sizes, rather than the held reference. On an unforced refresh those true sizes are controlled by the paid charge.

    theorem true_charge {δ b x y : ℝ} (hδ : 0 ≤ δ) (hy : 0 ≤ y)
    (hcmp : compared δ b x) (hne : b ≠ relativeUpdate δ b y) :
    x+y ≤ (1+δ)*charge b (relativeUpdate δ b y) := by
…