OAI/Combinatorics/UniformKServer/PilotFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite pilot family constants: the tier weights sum independently of the number of tiers and of k.

  1. abbrev OAI.UniformKServer.PilotFamily.Index line 15
  2. def OAI.UniformKServer.PilotFamily.template line 17
  3. def OAI.UniformKServer.PilotFamily.weight line 21
  4. theorem OAI.UniformKServer.PilotFamily.weight_nonneg line 25
  5. theorem OAI.UniformKServer.PilotFamily.weight_sum line 28
  6. def OAI.UniformKServer.PilotFamily.rateBound line 34
  7. theorem OAI.UniformKServer.PilotFamily.rate_bound line 36
  8. theorem OAI.UniformKServer.PilotFamily.rateBound_nonneg line 46