OAI/Combinatorics/UniformKServer/ActualRoundingChain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Adapted rounded joint laws for the literal partition/allocation process, with the exact financed movement bound.

  1. theorem OAI.UniformKServer.PartitionTree.allocation_causal line 17
  2. theorem OAI.UniformKServer.PartitionTree.anchors_causal line 29
  3. def OAI.UniformKServer.PartitionTree.roundingChain line 38
  4. theorem OAI.UniformKServer.PartitionTree.roundingChain_cost line 54