OAI/Combinatorics/UniformKServer/OffsetParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Terminating rational search for the restart length. The uniform finite-law endpoint is used only to prove termination, never supplied to the constructor.

  1. def OAI.UniformKServer.OffsetParameters.cap line 17
  2. def OAI.UniformKServer.OffsetParameters.acceptable line 20
  3. instance OAI.UniformKServer.OffsetParameters.acceptableDecidable line 24
  4. theorem OAI.UniformKServer.OffsetParameters.search_exists line 27
  5. def OAI.UniformKServer.OffsetParameters.restart line 46
  6. theorem OAI.UniformKServer.OffsetParameters.restart_spec line 51
  7. theorem OAI.UniformKServer.OffsetParameters.cap_bound line 56
  8. theorem OAI.UniformKServer.OffsetParameters.overhead_bound line 67