OAI/Combinatorics/UniformKServer/StarSchedules.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The source star's actual causal data: persistent held sizes, parent refresh, epochs, upper parameter and coarse dominant flexible-mass tracker.

  1. theorem OAI.UniformKServer.StarSchedules.refining line 20
  2. theorem OAI.UniformKServer.StarSchedules.estimate_measurable line 26
  3. theorem OAI.UniformKServer.StarSchedules.held_measurable line 31
  4. theorem OAI.UniformKServer.StarSchedules.parent_estimate_measurable line 42
  5. theorem OAI.UniformKServer.StarSchedules.parent_reference_measurable line 49
  6. def OAI.UniformKServer.StarSchedules.parentRefresh line 57
  7. theorem OAI.UniformKServer.StarSchedules.refresh_measurable line 60
  8. def OAI.UniformKServer.StarSchedules.epoch line 66
  9. theorem OAI.UniformKServer.StarSchedules.epoch_valid line 69
  10. theorem OAI.UniformKServer.StarSchedules.epoch_measurable line 73
  11. def OAI.UniformKServer.StarSchedules.upper line 78
  12. theorem OAI.UniformKServer.StarSchedules.upper_measurable line 81
  13. theorem OAI.UniformKServer.StarSchedules.upper_allowed line 86
  14. theorem OAI.UniformKServer.StarSchedules.flag_measurable line 90
  15. theorem OAI.UniformKServer.StarSchedules.flex_measurable line 96
  16. def OAI.UniformKServer.StarSchedules.deficit line 105
  17. theorem OAI.UniformKServer.StarSchedules.deficit_nonneg line 110
  18. theorem OAI.UniformKServer.StarSchedules.deficit_measurable line 121
  19. theorem OAI.UniformKServer.StarSchedules.core_measurable line 129