OAI/Combinatorics/UniformKServer/PilotTemplates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual admissible pilot templates; no drift/pilot premise is added to the partition construction. The constants are independent of the finite law.

  1. def OAI.UniformKServer.PilotEdits.smallGamma line 16
  2. theorem OAI.UniformKServer.PilotEdits.smallGamma_pos line 18
  3. def OAI.UniformKServer.PilotEdits.scaleShift line 22
  4. theorem OAI.UniformKServer.PilotEdits.shift_valid line 24
  5. def OAI.UniformKServer.PilotEdits.template line 33
  6. def OAI.UniformKServer.PilotEdits.heavyTemplate line 51
  7. def OAI.UniformKServer.PilotEdits.shortTemplate line 52
  8. theorem OAI.UniformKServer.PilotEdits.rate_nonneg line 55