OAI/Combinatorics/UniformKServer/UniformParameters.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The source's freely chosen small constants are fixed once and for all. The parent construction has one absolute squared-log coefficient.

  1. def OAI.UniformKServer.PartitionTree.fixedPilot line 16
  2. def OAI.UniformKServer.PartitionTree.fixedExponent line 30
  3. def OAI.UniformKServer.PartitionTree.fixedShift line 31
  4. def OAI.UniformKServer.PartitionTree.fixedConfig line 33
  5. def OAI.UniformKServer.PartitionTree.metricRadius line 47
  6. theorem OAI.UniformKServer.PartitionTree.metricRadius_pos line 49
  7. theorem OAI.UniformKServer.PartitionTree.metricRadius_bounds line 54
  8. theorem OAI.UniformKServer.PartitionTree.terminal_scale line 61
  9. def OAI.UniformKServer.PartitionTree.allocationScalar line 78
  10. def OAI.UniformKServer.PartitionTree.driftScalar line 81
  11. def OAI.UniformKServer.PartitionTree.rawRate line 83
  12. theorem OAI.UniformKServer.PartitionTree.editBound_nonneg line 87
  13. theorem OAI.UniformKServer.PartitionTree.allocationScalar_nonneg line 91
  14. theorem OAI.UniformKServer.PartitionTree.driftScalar_pos line 96
  15. theorem OAI.UniformKServer.PartitionTree.rawRate_nonneg line 101
  16. theorem OAI.UniformKServer.PartitionTree.rate_quadratic line 109
  17. def OAI.UniformKServer.PartitionTree.logFactor line 134
  18. theorem OAI.UniformKServer.PartitionTree.ell_log line 136
  19. theorem OAI.UniformKServer.PartitionTree.rate_logSquared line 145
  20. def OAI.UniformKServer.PartitionTree.absoluteRate line 159

    Source documentation

    This coefficient contains only the fixed numerical parameters, never an instance size, aspect ratio, tree height, hidden law, or horizon.

    def absoluteRate : ℝ := rawRate (fixedConfig (X:=PUnit) 1 (by norm_num) PUnit.unit)*logFactor^2

    Mentions: OAI.UniformKServer.PartitionTree.rawRate, OAI.UniformKServer.PartitionTree.fixedConfig, OAI.UniformKServer.PartitionTree.logFactor

  21. theorem OAI.UniformKServer.PartitionTree.rawRate_fixed line 161
  22. theorem OAI.UniformKServer.PartitionTree.fixed_rate line 164
  23. theorem OAI.UniformKServer.PartitionTree.absoluteRate_nonneg line 169