OAI/Combinatorics/UniformKServer/HeavyBirths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Input-determined birth times for current heavy centers. Labels and radii may be random, but their center's birth coordinate never depends on that randomness.

  1. def OAI.UniformKServer.HeavyProcess.births line 17
  2. theorem OAI.UniformKServer.HeavyProcess.run_birth line 22