OAI/Combinatorics/UniformKServer/ActualAllocationBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete common-tree allocator paid by true metric movement.

  1. theorem OAI.UniformKServer.PartitionTree.expect_average line 16
  2. theorem OAI.UniformKServer.PartitionTree.allocation_finance line 27