OAI/Combinatorics/UniformKServer/ParkedTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal one-step matching realization of joint tree rounding. The coincident-label charge is restricted to labels occupied at both times.

  1. def OAI.UniformKServer.TreeRounding.Realization.permute line 17
  2. def OAI.UniformKServer.TreeRounding.commonDistance line 23
  3. theorem OAI.UniformKServer.TreeRounding.commonDistance_nonneg line 26
  4. theorem OAI.UniformKServer.TreeRounding.parked_matching line 29
  5. theorem OAI.UniformKServer.TreeRounding.mean_intPark line 73