OAI/Combinatorics/KServer/FiniteLaw.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Absolute constants for the unconditional finite-law endpoint. No metric, finite-tree depth, horizon, law or initial tuple enters these coefficients.

  1. def OAI.KServer.GlobalEndpoint.core line 15
  2. def OAI.KServer.GlobalEndpoint.cutoff line 16
  3. def OAI.KServer.GlobalEndpoint.quotaMultiplier line 17
  4. def OAI.KServer.GlobalEndpoint.keyMultiplier line 18
  5. def OAI.KServer.GlobalEndpoint.optMultiplier line 19
  6. def OAI.KServer.GlobalEndpoint.embA line 21
  7. def OAI.KServer.GlobalEndpoint.embB line 22
  8. def OAI.KServer.GlobalEndpoint.embC line 23
  9. def OAI.KServer.GlobalEndpoint.embeddingMultiplier line 25
  10. def OAI.KServer.GlobalEndpoint.competitiveMultiplier line 26
  11. lemma OAI.KServer.GlobalEndpoint.constants_pos line 28
  12. lemma OAI.KServer.GlobalEndpoint.embedding_coefficient line 42
  13. def OAI.KServer.GlobalEndpoint.radii line 83
  14. lemma OAI.KServer.GlobalEndpoint.radii_pos line 84
  15. def OAI.KServer.GlobalEndpoint.quotaInventory line 87
  16. def OAI.KServer.GlobalEndpoint.chargeInventory line 90
  17. def OAI.KServer.GlobalEndpoint.potentialInventory line 93
  18. def OAI.KServer.GlobalEndpoint.embeddingInventory line 94
  19. def OAI.KServer.GlobalEndpoint.baseInventory line 96
  20. def OAI.KServer.GlobalEndpoint.inventory line 99
  21. lemma OAI.KServer.GlobalEndpoint.opt_nonneg line 105
  22. lemma OAI.KServer.GlobalEndpoint.cost_by_keys line 109
  23. lemma OAI.KServer.GlobalEndpoint.finite_geometric line 184
  24. lemma OAI.KServer.GlobalEndpoint.finite_scales line 226