OAI/Combinatorics/UniformKServer/HeavySeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Physical separation by the actual disjoint heavy balls. No factor equal to the number of records is lost: for a short edge there is at most one possible boundary ball, and its single birth-coordinate marginal is uniform.

  1. theorem OAI.UniformKServer.HeavyRecords.key_eq_iff line 23
  2. theorem OAI.UniformKServer.HeavyRecords.key_ne_witness line 42
  3. theorem OAI.UniformKServer.HeavyRecords.near_boundary line 53
  4. theorem OAI.UniformKServer.HeavyRecords.static_separation line 63