IntersectionLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the actual finite-tail intersection volumes.

def OAI.TotientAsymptotic.intersectionWeight line 13
lemma OAI.TotientAsymptotic.normalized_intersection_expression_limit line 17
theorem OAI.TotientAsymptotic.normalized_intersection_volume_limit line 62
Source documentation
Each genuine intersection volume has its stated coefficient limit. The hypothesis concerns only a fixed finite set of tail witnesses.
```
theorem normalized_intersection_volume_limit (hford : FordRenewalInput)
    {H : ℕ} {s : ℝ} (T : Finset (TailDatum H)) (hne : T.Nonempty)
    (hT : ∀ η ∈ T, IsWitness H s η) :
    Tendsto (fun x : ℝ => (volume (tailIntersection x H T)).toReal/G x (m x) -
      intersectionWeight (theta x) T) atTop (nhds 0) := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.tailIntersection, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.intersectionWeight, OAI.TotientAsymptotic.theta