OAI/Combinatorics/UniformKServer/PartitionMovement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Movement of the actual allocation on the actual common tree, reduced to literal coordinate-key edits. All addends are uniform in hidden law/horizon.

  1. def OAI.UniformKServer.PartitionTree.weight line 19
  2. theorem OAI.UniformKServer.PartitionTree.radius_step line 23
  3. theorem OAI.UniformKServer.PartitionTree.weight_separated line 32
  4. def OAI.UniformKServer.PartitionTree.coordinateCost line 38
  5. theorem OAI.UniformKServer.PartitionTree.pointwise_hidden line 44
  6. theorem OAI.UniformKServer.PartitionTree.hidden_bound line 70
  7. theorem OAI.UniformKServer.PartitionTree.actual_movement line 113