OAI/Combinatorics/UniformKServer/LevelMassLedger.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Linear auxiliary-potential accounting for a stationary submass and one unit designated mover. The mover is charged separately from post-request mass.

  1. def OAI.UniformKServer.LevelMap.Data.editCost line 20
  2. def OAI.UniformKServer.LevelMap.Data.auxiliary line 23
  3. def OAI.UniformKServer.LevelMap.Data.stationaryAllowance line 26
  4. def OAI.UniformKServer.LevelMap.Data.moverAllowance line 29
  5. theorem OAI.UniformKServer.LevelMap.Data.auxiliary_stationary line 32
  6. theorem OAI.UniformKServer.LevelMap.Data.auxiliary_mover line 38
  7. theorem OAI.UniformKServer.LevelMap.Data.mass_ledger line 44
  8. theorem OAI.UniformKServer.LevelMap.Data.auxiliary_bounds line 63