OAI/Combinatorics/UniformKServer/StarConstants.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

One absolute choice in the source's ordered smallness requirements. All parameters remain independent of the star, k, law and horizon.

  1. def OAI.UniformKServer.StarConstants.delta line 14
  2. def OAI.UniformKServer.StarConstants.rho line 15
  3. def OAI.UniformKServer.StarConstants.lam line 16
  4. def OAI.UniformKServer.StarConstants.eps line 17
  5. def OAI.UniformKServer.StarConstants.ct line 18
  6. def OAI.UniformKServer.StarConstants.cw line 19
  7. def OAI.UniformKServer.StarConstants.multiplier line 20
  8. theorem OAI.UniformKServer.StarConstants.delta_bounds line 22
  9. theorem OAI.UniformKServer.StarConstants.rho_bounds line 23
  10. theorem OAI.UniformKServer.StarConstants.lam_bounds line 24
  11. theorem OAI.UniformKServer.StarConstants.eps_pos line 25
  12. theorem OAI.UniformKServer.StarConstants.fine_error line 26
  13. theorem OAI.UniformKServer.StarConstants.fine_gap line 28
  14. theorem OAI.UniformKServer.StarConstants.fine_eps line 29
  15. theorem OAI.UniformKServer.StarConstants.ct_pos line 30
  16. theorem OAI.UniformKServer.StarConstants.ct_height line 31
  17. theorem OAI.UniformKServer.StarConstants.multiplier_bound line 32
  18. theorem OAI.UniformKServer.StarConstants.cw_pos line 33
  19. theorem OAI.UniformKServer.StarConstants.cw_height line 34