FirstHitSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Required finite-law partition bridge: only potentially hitting roster records are charged in the truncated-radius correction. All other present records remain in the actual chronological product experiment.

theorem OAI.UniformKServer.FirstHit.separationProbability_nonneg line 17
theorem OAI.UniformKServer.FirstHit.separationProbability_le_hit line 20
theorem OAI.UniformKServer.FirstHit.first_hit_error_sum line 33
Source documentation
A support-sensitive version of the first-hit telescope. The main term still telescopes to one; only the sum of tail errors is charged.
```
theorem first_hit_error_sum (es : List Entry) (α : ℝ) (ε : Entry → ℝ)
    (hα : 0 ≤ α) (hε : ∀ E ∈ es, 0 ≤ ε E)
    (hlocal : ∀ E ∈ es, separationProbability E ≤ α*(hitProbability E+ε E)) :
    (experiment es).expect (fun ω => if firstSeparates es ω then 1 else 0) ≤
      α*(1+(es.map ε).sum) := by
…
```
Mentions: OAI.UniformKServer.FirstHit.Entry, OAI.UniformKServer.FirstHit.separationProbability, OAI.UniformKServer.FirstHit.hitProbability, OAI.UniformKServer.FirstHit.experiment, OAI.UniformKServer.FirstHit.firstSeparates

theorem OAI.UniformKServer.FirstHit.first_hit_support line 63

Source documentation

A heterogeneous indexed formulation avoids identifying equal physical centers or equal entry laws; repeated centers are counted as separate records.

theorem first_hit_support {I : Type*} (is : List I) (entry : I → Entry)
    (P : I → Prop) (α ε : ℝ) (hα : 0 ≤ α) (hε : 0 ≤ ε)
    (hlocal : ∀ i ∈ is, P i →
      separationProbability (entry i) ≤ α*(hitProbability (entry i)+ε))
    (hmiss : ∀ i ∈ is, ¬ P i → hitProbability (entry i) = 0) :
    (experiment (is.map entry)).expect (fun ω => if firstSeparates _ ω then 1 else 0) ≤
      α*(1+((is.filter (fun i => decide (P i))).length:ℝ)*ε) := by
…

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