OAI/Combinatorics/UniformKServer/IntegerParks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A rounded, consistent hierarchy contains exactly k integer parks. Their literal labeled enumeration has the prescribed subtree counts.

  1. theorem OAI.UniformKServer.TreeRounding.rounded_nonneg line 17
  2. theorem OAI.UniformKServer.TreeRounding.rounded_park_nonneg line 21
  3. def OAI.UniformKServer.TreeRounding.integerAllocation line 25
  4. theorem OAI.UniformKServer.TreeRounding.intPark_total line 31
  5. theorem OAI.UniformKServer.TreeRounding.intPark_subtree line 37
  6. theorem OAI.UniformKServer.TreeRounding.intPark_nat_total line 41
  7. structure OAI.UniformKServer.TreeRounding.Realization line 48
  8. theorem OAI.UniformKServer.TreeRounding.realization_exists line 53
  9. def OAI.UniformKServer.TreeRounding.realize line 76
  10. theorem OAI.UniformKServer.TreeRounding.Realization.subtree line 79
  11. theorem OAI.UniformKServer.TreeRounding.Realization.valid line 86