OAI/Combinatorics/UniformKServer/SideFiniteLedger.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

All-step side ledger with actual affine posterior coefficients fixed before refresh. No posterior-ratio variation or after-refresh filtering is used.

  1. def OAI.UniformKServer.SideFiniteLedger.potential line 19
  2. def OAI.UniformKServer.SideFiniteLedger.movement line 21
  3. def OAI.UniformKServer.SideFiniteLedger.jump line 23
  4. def OAI.UniformKServer.SideFiniteLedger.coefficient line 26
  5. theorem OAI.UniformKServer.SideFiniteLedger.coefficient_bound line 30
  6. theorem OAI.UniformKServer.SideFiniteLedger.coefficient_measurable line 37
  7. theorem OAI.UniformKServer.SideFiniteLedger.frozen_change line 46
  8. theorem OAI.UniformKServer.SideFiniteLedger.step_bound line 75
  9. theorem OAI.UniformKServer.SideFiniteLedger.budget line 112