OAI/Combinatorics/UniformKServer/StarParameters.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic child/parent parameter gaps for the actual finite-count star. The only epoch input is the invariant of the concrete held-size schedule.

  1. def OAI.UniformKServer.StarParameters.childSize line 19
  2. def OAI.UniformKServer.StarParameters.parentSize line 21
  3. theorem OAI.UniformKServer.StarParameters.size_nonneg line 24
  4. theorem OAI.UniformKServer.StarParameters.positive_accuracy line 29
  5. theorem OAI.UniformKServer.StarParameters.size_with_side line 46
  6. theorem OAI.UniformKServer.StarParameters.child_le_parent line 67
  7. theorem OAI.UniformKServer.StarParameters.size_ratio line 73
  8. theorem OAI.UniformKServer.StarParameters.beta_difference line 81
  9. theorem OAI.UniformKServer.StarParameters.regular_gap line 95
  10. theorem OAI.UniformKServer.StarParameters.dominant_gap line 120