OAI/Combinatorics/UniformKServer/ActualAnchorTravel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Literal metric movement of retained heavy anchors, weighted by the new parked mass. This is the travel used when projecting rounded tree servers.

  1. theorem OAI.UniformKServer.LevelMap.Data.anchor_distance line 17
  2. def OAI.UniformKServer.PartitionTree.anchorTravel line 38
  3. theorem OAI.UniformKServer.PartitionTree.anchorTravel_le line 46
  4. def OAI.UniformKServer.PartitionTree.totalAnchorTravel line 66
  5. theorem OAI.UniformKServer.PartitionTree.totalAnchorTravel_le line 69