OAI/Combinatorics/UniformKServer/StarOutputMovement.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal non-wholesale output movement with coefficient one on the parent. The switch charge is the actual causal hysteresis charge.

  1. def OAI.UniformKServer.StarOutputMovement.alphaMove line 19
  2. def OAI.UniformKServer.StarOutputMovement.sideMove line 21
  3. def OAI.UniformKServer.StarOutputMovement.deficitMove line 23
  4. def OAI.UniformKServer.StarOutputMovement.expense line 25
  5. theorem OAI.UniformKServer.StarOutputMovement.parts_nonneg line 28
  6. theorem OAI.UniformKServer.StarOutputMovement.one_move line 35
  7. theorem OAI.UniformKServer.StarOutputMovement.two_move line 50
  8. theorem OAI.UniformKServer.StarOutputMovement.down_move line 64
  9. theorem OAI.UniformKServer.StarOutputMovement.up_move line 82
  10. theorem OAI.UniformKServer.StarOutputMovement.rule_move line 101