RadiusRoster.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The first-hit estimate for the entire actual present roster. The global roster may have far more than K² records. Only centers that can hit one of the two points incur a truncated-tail correction; all other coordinates remain in the actual independent product law.

theorem OAI.UniformKServer.RadiusRoster.candidate_count line 24

Source documentation

Repeated centers are distinct chronological identities, not collapsed into a set of sites. This count therefore applies to the actual roster.

theorem candidate_count (S : Finset I) (is : List I) (c : I → X) (r : ℝ)
    (A : ℕ) (x y : X) (hr : 0 ≤ r) (hxy : dist x y ≤ r)
    (hnodup : is.Nodup) (hsub : ∀ i ∈ is, i ∈ S)
    (hage : ∀ i ∈ is, ChronologicalRoster.age S c r i < A) :
    (is.filter (fun i => decide (dist (c i) x ≤ 2*r ∨ dist (c i) y ≤ 2*r))).length ≤ A := by
…

Mentions: OAI.UniformKServer.ChronologicalRoster.age

theorem OAI.UniformKServer.RadiusRoster.hit_zero line 50
Source documentation
Outside the geometric support the hit probability is exactly zero. The endpoint convention matches the zero tail at 2r.
```
theorem hit_zero (lam r : ℝ) (hlam : 0 < lam) (hr : 0 < r) (c x y : X)
    (hx : 2*r ≤ dist c x) (hy : 2*r ≤ dist c y) :
    FirstHit.hitProbability (RadiusFirstHit.entry lam r c x y) = 0 := by
…
```
Mentions: OAI.UniformKServer.FirstHit.hitProbability, OAI.UniformKServer.RadiusFirstHit.entry

theorem OAI.UniformKServer.RadiusRoster.present_first_hit line 64

Source documentation

Source lemma first-hit, with the real chronological age hypothesis rather than a false bound on the length of the whole present roster.

theorem present_first_hit (S : Finset I) (is : List I) (c : I → X)
    (K : ℕ) (hK : 2 ≤ K) (r : ℝ) (hr : 0 < r) (x y : X)
    (hxy : dist x y < r/4) (hnodup : is.Nodup)
    (hsub : ∀ i ∈ is, i ∈ S)
    (hage : ∀ i ∈ is, ChronologicalRoster.age S c r i < K^2) :
    (FirstHit.experiment (is.map (fun i =>
      RadiusFirstHit.entry (Real.log (1+(K:ℝ)^2)) r (c i) 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.ChronologicalRoster.age, OAI.UniformKServer.FirstHit.experiment, OAI.UniformKServer.RadiusFirstHit.entry, OAI.UniformKServer.FirstHit.firstSeparates