OAI/Combinatorics/UniformKServer/EpochAlphaSchedule.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual total choice of the epoch proportions, including the empty branch. Validity is derived from the persistent epoch and forced side-reference recurrences; the inactive or zero-side cases are not excluded.

  1. def OAI.UniformKServer.EpochAlphaSchedule.config line 20
  2. theorem OAI.UniformKServer.EpochAlphaSchedule.dominant_active line 30
  3. theorem OAI.UniformKServer.EpochAlphaSchedule.active_eq line 38
  4. theorem OAI.UniformKServer.EpochAlphaSchedule.valid_config line 52
  5. theorem OAI.UniformKServer.EpochAlphaSchedule.base_bound line 75
  6. def OAI.UniformKServer.EpochAlphaSchedule.schedule line 87
  7. theorem OAI.UniformKServer.EpochAlphaSchedule.schedule_valid line 92
  8. theorem OAI.UniformKServer.EpochAlphaSchedule.schedule_active line 105