OAI/Combinatorics/UniformKServer/RawControllerCost.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.RawControllerCost.u line 20
  2. theorem OAI.UniformKServer.RawControllerCost.u_injective line 23
  3. def OAI.UniformKServer.RawControllerCost.N line 27
  4. theorem OAI.UniformKServer.RawControllerCost.total line 31
  5. theorem OAI.UniformKServer.RawControllerCost.lazy line 35
  6. def OAI.UniformKServer.RawControllerCost.expected line 38
  7. def OAI.UniformKServer.RawControllerCost.slope line 43
  8. def OAI.UniformKServer.RawControllerCost.endpoint line 45
  9. theorem OAI.UniformKServer.RawControllerCost.endpoint_nonneg line 49
  10. theorem OAI.UniformKServer.RawControllerCost.suffix line 56
  11. theorem OAI.UniformKServer.RawControllerCost.coefficient_bound line 95
  12. def OAI.UniformKServer.RawControllerCost.delayed line 101
  13. theorem OAI.UniformKServer.RawControllerCost.delayed_bound line 106