OAI/Combinatorics/UniformKServer/TreeAllocator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Top-down propagation on the fixed finite tree, with literal causal star outputs. Repeated and empty leaf counts are not excluded.

  1. def OAI.UniformKServer.TreeAllocator.amount line 18
  2. theorem OAI.UniformKServer.TreeAllocator.root line 24
  3. theorem OAI.UniformKServer.TreeAllocator.child line 27
  4. theorem OAI.UniformKServer.TreeAllocator.lower_le line 33
  5. theorem OAI.UniformKServer.TreeAllocator.parent_le line 49
  6. theorem OAI.UniformKServer.TreeAllocator.nonneg line 53
  7. theorem OAI.UniformKServer.TreeAllocator.budget line 56
  8. def OAI.UniformKServer.TreeAllocator.allocation line 61
  9. theorem OAI.UniformKServer.TreeAllocator.measurable line 67