OAI/Combinatorics/UniformKServer/HeavyRecords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Fixed-slot implementation of disjoint heavy balls, including the literal finite-metric intersection test for label reuse.

  1. structure OAI.UniformKServer.HeavyRecords.State line 16
  2. def OAI.UniformKServer.HeavyRecords.covers line 25
  3. theorem OAI.UniformKServer.HeavyRecords.unique line 29
  4. def OAI.UniformKServer.HeavyRecords.key line 37
  5. theorem OAI.UniformKServer.HeavyRecords.key_some line 40
  6. theorem OAI.UniformKServer.HeavyRecords.key_none line 52
  7. def OAI.UniformKServer.HeavyRecords.intersects line 56
  8. theorem OAI.UniformKServer.HeavyRecords.intersect_distance line 60
  9. theorem OAI.UniformKServer.HeavyRecords.intersect_unique line 68
  10. def OAI.UniformKServer.HeavyRecords.reused line 78
  11. def OAI.UniformKServer.HeavyRecords.chosen line 81
  12. theorem OAI.UniformKServer.HeavyRecords.chosen_of_intersects line 84
  13. theorem OAI.UniformKServer.HeavyRecords.chosen_cases line 90
  14. def OAI.UniformKServer.HeavyRecords.survivors line 98
  15. theorem OAI.UniformKServer.HeavyRecords.chosen_not_survivor line 101
  16. def OAI.UniformKServer.HeavyRecords.insert line 110
  17. theorem OAI.UniformKServer.HeavyRecords.new_covers line 142
  18. theorem OAI.UniformKServer.HeavyRecords.covers_insert_iff line 149
  19. theorem OAI.UniformKServer.HeavyRecords.center_injective line 163
  20. theorem OAI.UniformKServer.HeavyRecords.card_present line 172