OAI/Combinatorics/UniformKServer/FiniteLawFinance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The assembled finite-law bound: the policy is a legal causal flow, the coefficient is absolute squared-logarithmic, and the additive quantity knows neither the horizon nor the request law.

  1. def OAI.UniformKServer.PartitionTree.flowServe line 16
  2. theorem OAI.UniformKServer.PartitionTree.avg_range line 21
  3. theorem OAI.UniformKServer.PartitionTree.avg_constant line 25
  4. def OAI.UniformKServer.PartitionTree.lawFlow line 28
  5. theorem OAI.UniformKServer.PartitionTree.lawFlow_valid line 34
  6. def OAI.UniformKServer.PartitionTree.flowEndpoint line 45
  7. theorem OAI.UniformKServer.PartitionTree.component_average line 48
  8. theorem OAI.UniformKServer.PartitionTree.lawFlow_bound line 69
  9. theorem OAI.UniformKServer.PartitionTree.fixed_lawFlow_bound line 88