OAI/Combinatorics/UniformKServer/LevelKeyLedger.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Full level key edits with the genuine heavy-first serial auxiliary potential.

  1. def OAI.UniformKServer.LevelMap.Data.keyPotential line 21
  2. def OAI.UniformKServer.LevelMap.Data.heavyStationaryBudget line 24
  3. def OAI.UniformKServer.LevelMap.Data.heavyMoverBudget line 27
  4. theorem OAI.UniformKServer.LevelMap.Data.key_ledger line 31
  5. theorem OAI.UniformKServer.LevelMap.Data.key_stationary line 54
  6. theorem OAI.UniformKServer.LevelMap.Data.key_mover line 61