OAI/Combinatorics/UniformKServer/StarOutputFeasibility.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual feasibility of both child-output formulas, at every positive time. Regime inequalities are the literal hysteresis ranges. Degenerate active, side, core and deficit values are not removed.

  1. def OAI.UniformKServer.StarOutputFeasibility.one line 18
  2. def OAI.UniformKServer.StarOutputFeasibility.two line 21
  3. theorem OAI.UniformKServer.StarOutputFeasibility.one_inactive line 25
  4. theorem OAI.UniformKServer.StarOutputFeasibility.one_lower line 30
  5. theorem OAI.UniformKServer.StarOutputFeasibility.one_upper line 64
  6. theorem OAI.UniformKServer.StarOutputFeasibility.one_budget line 68
  7. theorem OAI.UniformKServer.StarOutputFeasibility.side_upper line 79
  8. theorem OAI.UniformKServer.StarOutputFeasibility.side_lower line 90
  9. theorem OAI.UniformKServer.StarOutputFeasibility.two_lower line 118
  10. theorem OAI.UniformKServer.StarOutputFeasibility.two_upper line 148
  11. theorem OAI.UniformKServer.StarOutputFeasibility.two_budget line 153