OAI/Combinatorics/UniformKServer/LevelErrorMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual stationary posterior errors are charged to the insertion masses. The designated mover is not incorrectly treated as post-request mass.

  1. theorem OAI.UniformKServer.PartitionLevel.Input.heavy_bridge line 19
  2. theorem OAI.UniformKServer.PartitionLevel.Input.error_mass_bound line 23
  3. theorem OAI.UniformKServer.PartitionLevel.Input.stationary_tier_charge line 50
  4. theorem OAI.UniformKServer.PartitionLevel.Input.stationary_heavy_charge line 68