OAI/Combinatorics/UniformKServer/PilotCredits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.PilotCompact.coarseConstant line 10
2. theorem OAI.UniformKServer.PilotCompact.coarseConstant_nonneg line 15
3. theorem OAI.UniformKServer.PilotCompact.coarse_drift line 23
4. def OAI.UniformKServer.PilotCompact.driftConstant line 73

   Source documentation

   The constant in companion Lemma pilot-drift.

   def driftConstant (σ γ δ L : ℝ) (p : ℕ) : ℝ :=
   …

5. theorem OAI.UniformKServer.PilotCompact.driftConstant_log line 77
6. theorem OAI.UniformKServer.PilotCompact.scale_cut line 108
7. theorem OAI.UniformKServer.PilotCompact.small_drift line 122