OAI/Combinatorics/UniformKServer/OffsetInstance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Uniform absolute squared-log cost for the exact rational-search/dyadic suffix, with arbitrary repeated starts and arbitrary finite activation delay. The literal bit-machine implementation is deliberately not asserted here.

  1. theorem OAI.UniformKServer.OffsetInstance.history_diameter line 17
  2. def OAI.UniformKServer.OffsetInstance.slope line 32
  3. theorem OAI.UniformKServer.OffsetInstance.rate_bound line 36
  4. def OAI.UniformKServer.OffsetInstance.restart line 40
  5. def OAI.UniformKServer.OffsetInstance.cap line 43
  6. theorem OAI.UniformKServer.OffsetInstance.valid line 47
  7. theorem OAI.UniformKServer.OffsetInstance.restart_pos line 55
  8. def OAI.UniformKServer.OffsetInstance.expected line 59
  9. def OAI.UniformKServer.OffsetInstance.endpoint line 65
  10. theorem OAI.UniformKServer.OffsetInstance.endpoint_nonneg line 70
  11. theorem OAI.UniformKServer.OffsetInstance.suffix_bound line 78
  12. def OAI.UniformKServer.OffsetInstance.coefficient line 94
  13. theorem OAI.UniformKServer.OffsetInstance.coefficient_positive line 96
  14. theorem OAI.UniformKServer.OffsetInstance.coefficient_bound line 103
  15. def OAI.UniformKServer.OffsetInstance.delayedCost line 116
  16. theorem OAI.UniformKServer.OffsetInstance.delayed_bound line 121