OAI/Combinatorics/UniformKServer/OfflineLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

No hidden-trajectory hypothesis is added: an optimal finite serving history is selected for each atom of an arbitrary finite request law.

  1. def OAI.UniformKServer.OfflineLaw.history line 18
  2. theorem OAI.UniformKServer.OfflineLaw.history_map line 21
  3. theorem OAI.UniformKServer.OfflineLaw.history_cost line 24
  4. theorem OAI.UniformKServer.OfflineLaw.history_length line 29
  5. def OAI.UniformKServer.OfflineLaw.data line 33
  6. theorem OAI.UniformKServer.OfflineLaw.data_public line 38
  7. theorem OAI.UniformKServer.OfflineLaw.support_nonempty line 41
  8. theorem OAI.UniformKServer.OfflineLaw.data_trace line 50
  9. theorem OAI.UniformKServer.OfflineLaw.data_cost line 56
  10. theorem OAI.UniformKServer.PartitionTree.literal_valid line 85
  11. theorem OAI.UniformKServer.PartitionTree.literal_bound line 92