TailPower.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential limit of the finite-tail simplex factor, uniformly in phase.

lemma OAI.TotientAsymptotic.tailBudget_nonneg line 14
theorem OAI.TotientAsymptotic.tail_simplex_power_limit line 28
Source documentation
The exact power appearing in each intersection volume tends to its phase-dependent exponential weight; no continuity in the phase is assumed.
```
theorem tail_simplex_power_limit (hford : FordRenewalInput)
    {H : ℕ} {s : ℝ} (T : Finset (TailDatum H))
    (hT : ∀ η ∈ T, IsWitness H s η) :
    Tendsto (fun x : ℝ =>
      (max (1-tailBudget x H T/B x) 0)^(R x H) -
      Real.exp (-(gamma/alpha (theta x)) *
        ∑' n : ℕ, rho^(H+n)*maxD (H+n) T)) atTop (nhds 0) := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.tailBudget, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.gamma, OAI.TotientAsymptotic.alpha, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.maxD