OAI/Combinatorics/UniformKServer/ParkScale.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual pointwise scale sum for parks, including points of zero posterior mass. Add one to each ball mass exactly as in the held-size denominator.

  1. def OAI.UniformKServer.ParkCoefficients.outer line 17
  2. def OAI.UniformKServer.ParkCoefficients.inner line 19
  3. def OAI.UniformKServer.ParkCoefficients.bad line 22
  4. theorem OAI.UniformKServer.ParkCoefficients.outer_one line 25
  5. theorem OAI.UniformKServer.ParkCoefficients.inner_one line 30
  6. theorem OAI.UniformKServer.ParkCoefficients.inner_outer line 35
  7. theorem OAI.UniformKServer.ParkCoefficients.outer_shift line 43
  8. theorem OAI.UniformKServer.ParkCoefficients.scale_logs line 55
  9. theorem OAI.UniformKServer.ParkCoefficients.bad_count line 65