OAI/Combinatorics/UniformKServer/FirstHit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniformKServer.FirstHit.Entry line 16

   Source documentation

   A finite independently sampled chronological family. Each coordinate can include a collapsed continuous radius law, so no count of random bits is claimed at this existence-only stage.

   structure Entry where
   …

2. def OAI.UniformKServer.FirstHit.Samples line 26
3. instance OAI.UniformKServer.FirstHit.samplesFinite line 30
4. def OAI.UniformKServer.FirstHit.experiment line 34
5. def OAI.UniformKServer.FirstHit.firstSeparates line 38
6. def OAI.UniformKServer.FirstHit.hitProbability line 42
7. def OAI.UniformKServer.FirstHit.separationProbability line 43
8. theorem OAI.UniformKServer.FirstHit.hitProbability_bounds line 44
9. theorem OAI.UniformKServer.FirstHit.recurrence line 51
10. theorem OAI.UniformKServer.FirstHit.first_hit_bound line 81

    Source documentation

    First-hit bound with no factor for the number of entries multiplying the main density term. The only count loss is on the truncated tail correction.

    theorem first_hit_bound (es : List Entry) (α ε : ℝ) (hα : 0 ≤ α) (hε : 0 ≤ ε)
        (hlocal : ∀ E ∈ es, separationProbability E ≤ α*(hitProbability E+ε)) :
        (experiment es).expect (fun ω => if firstSeparates es ω then 1 else 0) ≤
          α*(1+(es.length:ℝ)*ε)
     := by
    …

    Mentions: OAI.UniformKServer.FirstHit.Entry, OAI.UniformKServer.FirstHit.separationProbability, OAI.UniformKServer.FirstHit.hitProbability, OAI.UniformKServer.FirstHit.experiment, OAI.UniformKServer.FirstHit.firstSeparates