OAI/Combinatorics/UniformKServer/TreeParking.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Park conservation, subtree-cut capacities, and weighted park variation.

  1. theorem OAI.UniformKServer.TreeParking.weighted_identity line 16
  2. theorem OAI.UniformKServer.TreeParking.total line 21
  3. def OAI.UniformKServer.TreeParking.boundary line 31
  4. theorem OAI.UniformKServer.TreeParking.cut line 33
  5. theorem OAI.UniformKServer.TreeParking.cut_capacity line 50
  6. theorem OAI.UniformKServer.TreeParking.pointwise_variation line 56
  7. theorem OAI.UniformKServer.TreeParking.weighted_variation line 65