OAI/Combinatorics/UniformKServer/StarCaps.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The source's fine caps, instantiated with absolute tolerances and the actual causal held-size epochs. Endpoint trackers are never restarted.

  1. def OAI.UniformKServer.StarCaps.factor line 19
  2. def OAI.UniformKServer.StarCaps.flex line 23
  3. def OAI.UniformKServer.StarCaps.cap line 27
  4. def OAI.UniformKServer.StarCaps.wholesale line 30
  5. theorem OAI.UniformKServer.StarCaps.tolerance line 33
  6. theorem OAI.UniformKServer.StarCaps.factor_range line 40
  7. theorem OAI.UniformKServer.StarCaps.cap_eq line 51
  8. theorem OAI.UniformKServer.StarCaps.cap_nonneg line 55
  9. theorem OAI.UniformKServer.StarCaps.cap_bound line 61
  10. theorem OAI.UniformKServer.StarCaps.inactive_cap line 67
  11. theorem OAI.UniformKServer.StarCaps.regular line 73
  12. theorem OAI.UniformKServer.StarCaps.dominant line 82
  13. theorem OAI.UniformKServer.StarCaps.deficit_comparison line 98
  14. theorem OAI.UniformKServer.StarCaps.not_wholesale_parent line 105
  15. theorem OAI.UniformKServer.StarCaps.not_wholesale_upper line 113
  16. theorem OAI.UniformKServer.StarCaps.not_wholesale_factor line 121
  17. theorem OAI.UniformKServer.StarCaps.cap_step line 128