OAI/Combinatorics/UniformKServer/HeavyRecordGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual center-set projection and common-label properties of the finite-slot heavy-ball update.

  1. def OAI.UniformKServer.HeavyRecords.centers line 18
  2. theorem OAI.UniformKServer.HeavyRecords.centers_separated line 20
  3. theorem OAI.UniformKServer.HeavyRecords.centers_insert line 28
  4. theorem OAI.UniformKServer.HeavyRecords.common_region_reused line 47
  5. theorem OAI.UniformKServer.HeavyRecords.reused_distance line 57
  6. theorem OAI.UniformKServer.HeavyRecords.unchanged_far line 70
  7. theorem OAI.UniformKServer.HeavyRecords.fresh_exists line 92