OAI/Combinatorics/UniformKServer/HeavySchedule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The literal deterministic heavy-center recursion of companion §07. The update decision depends only on the request, posterior, and old centers, not on any radius, lifetime, allocation, or rounding variable.

  1. def OAI.UniformKServer.HeavySchedule.Separated line 18
  2. def OAI.UniformKServer.HeavySchedule.trigger line 21
  3. def OAI.UniformKServer.HeavySchedule.step line 24
  4. def OAI.UniformKServer.HeavySchedule.centers line 27
  5. theorem OAI.UniformKServer.HeavySchedule.update_separated line 31
  6. theorem OAI.UniformKServer.HeavySchedule.step_separated line 43
  7. theorem OAI.UniformKServer.HeavySchedule.centers_separated line 50
  8. theorem OAI.UniformKServer.HeavySchedule.coverage line 56
  9. theorem OAI.UniformKServer.HeavySchedule.centers_coverage line 67
  10. theorem OAI.UniformKServer.HeavySchedule.intersect_unique line 71
  11. theorem OAI.UniformKServer.HeavySchedule.near_unique line 80
  12. theorem OAI.UniformKServer.HeavySchedule.intersection_displacement line 85