OAI/Combinatorics/UniformKServer/AnchorBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Telescoping the actual retained-anchor potential, retaining the literal allocation and true key-coordinate costs until the final financing step.

  1. theorem OAI.UniformKServer.PartitionTree.variation_integral line 18
  2. theorem OAI.UniformKServer.PartitionTree.refresh_integral line 41
  3. theorem OAI.UniformKServer.PartitionTree.park_change_integral line 47
  4. def OAI.UniformKServer.PartitionTree.payments line 56
  5. theorem OAI.UniformKServer.PartitionTree.payment_budget line 59