OAI/Combinatorics/UniformKServer/StarTrackers.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The recursive minimizers instantiated with the finite hidden-count law and its literal held parameters, rather than an assumed allocator interface.

  1. def OAI.UniformKServer.StarTrackers.alphaParam line 19
  2. theorem OAI.UniformKServer.StarTrackers.alphaParam_measurable line 22
  3. theorem OAI.UniformKServer.StarTrackers.alphaParam_active line 27
  4. def OAI.UniformKServer.StarTrackers.alphaData line 31
  5. theorem OAI.UniformKServer.StarTrackers.alpha_post line 53
  6. theorem OAI.UniformKServer.StarTrackers.alpha_input line 57
  7. def OAI.UniformKServer.StarTrackers.sideParam line 61
  8. theorem OAI.UniformKServer.StarTrackers.sideParam_measurable line 64
  9. def OAI.UniformKServer.StarTrackers.sideFlags line 69
  10. theorem OAI.UniformKServer.StarTrackers.sideFlags_measurable line 72
  11. theorem OAI.UniformKServer.StarTrackers.side_core_le line 78
  12. def OAI.UniformKServer.StarTrackers.sideData line 88
  13. theorem OAI.UniformKServer.StarTrackers.side_post line 120