OAI/Combinatorics/UniformKServer/AllocationMovement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Companion §05, the exact non-wholesale hole identities and movement bounds. The coefficient of the parent variation is exactly one.

  1. theorem OAI.UniformKServer.AllocationOutputs.sum_difference_le line 17
  2. theorem OAI.UniformKServer.AllocationOutputs.excess_difference line 22
  3. theorem OAI.UniformKServer.AllocationOutputs.outputs_from_holes line 31
  4. theorem OAI.UniformKServer.AllocationOutputs.scalar_vector_movement line 41
  5. theorem OAI.UniformKServer.AllocationOutputs.rule_one_movement line 54
  6. def OAI.UniformKServer.AllocationOutputs.sideTotal line 67
  7. def OAI.UniformKServer.AllocationOutputs.sideVariation line 69
  8. def OAI.UniformKServer.AllocationOutputs.holesTwo line 71
  9. theorem OAI.UniformKServer.AllocationOutputs.side_total_difference line 74
  10. theorem OAI.UniformKServer.AllocationOutputs.side_variation_le line 79
  11. theorem OAI.UniformKServer.AllocationOutputs.holes_two_movement line 83
  12. theorem OAI.UniformKServer.AllocationOutputs.rule_two_holes line 100
  13. theorem OAI.UniformKServer.AllocationOutputs.rule_two_movement line 125