OAI/Combinatorics/UniformKServer/RadiusFirstHit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.RadiusFirstHit.coverage line 16
2. def OAI.UniformKServer.RadiusFirstHit.entry line 18
3. theorem OAI.UniformKServer.RadiusFirstHit.ordered_tail line 27
4. theorem OAI.UniformKServer.RadiusFirstHit.local_bound line 37
5. theorem OAI.UniformKServer.RadiusFirstHit.actual_first_hit line 61

   Source documentation

   The radius laws are constructed, not postulated. Chronological candidate count is used only in the tail correction, never multiplying the main term.

   theorem actual_first_hit (cs : List X) (K : ℕ) (hK : 2 ≤ K) (r : ℝ) (hr : 0 < r)
       (x y : X) (hcount : cs.length ≤ K^2) :
       (FirstHit.experiment (cs.map (fun c => entry (Real.log (1+(K:ℝ)^2)) r c x y))).expect
         (fun ω => if FirstHit.firstSeparates _ ω then 1 else 0) ≤
           2*Real.log (1+(K:ℝ)^2)*dist x y/r
    := by
   …

   Mentions: OAI.UniformKServer.FirstHit.experiment, OAI.UniformKServer.RadiusFirstHit.entry, OAI.UniformKServer.FirstHit.firstSeparates