OAI/Combinatorics/UniformKServer/StarFeasibilityParameters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Explicit room for the actual held parameters in the two output rules. The inequalities include arbitrarily small dominant side proportions.

  1. def OAI.UniformKServer.StarFeasibilityParameters.sideReference line 20
  2. theorem OAI.UniformKServer.StarFeasibilityParameters.side_valid_reference line 23
  3. def OAI.UniformKServer.StarFeasibilityParameters.alphaParam line 28
  4. def OAI.UniformKServer.StarFeasibilityParameters.sideParam line 31
  5. theorem OAI.UniformKServer.StarFeasibilityParameters.alpha_valid line 34
  6. theorem OAI.UniformKServer.StarFeasibilityParameters.side_valid line 38
  7. theorem OAI.UniformKServer.StarFeasibilityParameters.regular_room_algebra line 43
  8. theorem OAI.UniformKServer.StarFeasibilityParameters.regular_room line 66
  9. theorem OAI.UniformKServer.StarFeasibilityParameters.dominant_room line 83
  10. theorem OAI.UniformKServer.StarFeasibilityParameters.side_room line 110
  11. theorem OAI.UniformKServer.StarFeasibilityParameters.side_slack line 142