OAI/Combinatorics/UniformKServer/SwitchFiniteLedger.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

All-step switch charge ledger with BEFORE-refresh measurable coefficients. No stopping-event conditioning or posterior-ratio variation is used.

  1. def OAI.UniformKServer.SwitchFiniteLedger.expense line 17
  2. theorem OAI.UniformKServer.SwitchFiniteLedger.pointwise line 20
  3. theorem OAI.UniformKServer.SwitchFiniteLedger.step_bound line 46
  4. theorem OAI.UniformKServer.SwitchFiniteLedger.budget line 54