TailRenewal.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The normalized finite-tail budget and its renewal-convolution limit.

def OAI.TotientAsymptotic.tailSequence line 15
lemma OAI.TotientAsymptotic.tailBudget_eq_sum line 18
lemma OAI.TotientAsymptotic.renewalConvolution_tailSequence line 28
theorem OAI.TotientAsymptotic.normalized_tailBudget_tendsto line 59
Source documentation
The exact tail budget converges after multiplication by rho^m. This is the analytic numerator in the manuscript's finite-tail approximation.
```
theorem normalized_tailBudget_tendsto (hford : FordRenewalInput)
    {H : ℕ} {s : ℝ} (T : Finset (TailDatum H))
    (hT : ∀ η ∈ T, IsWitness H s η) :
    Tendsto (fun x : ℝ => rho^(m x)*tailBudget x H T) atTop
      (nhds (gamma * ∑' n : ℕ, rho^(H+n)*maxD (H+n) T)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.tailBudget, OAI.TotientAsymptotic.gamma, OAI.TotientAsymptotic.maxD
lemma OAI.TotientAsymptotic.alpha_ge_lam line 71
lemma OAI.TotientAsymptotic.phase_division_error line 76
theorem OAI.TotientAsymptotic.tailBudget_exponent_error line 93
Source documentation
The phase-dependent exponent in the simplex volume, before replacing m by the prefix dimension m-H.
```
theorem tailBudget_exponent_error (hford : FordRenewalInput)
    {H : ℕ} {s : ℝ} (T : Finset (TailDatum H))
    (hT : ∀ η ∈ T, IsWitness H s η) :
    Tendsto (fun x : ℝ => (m x : ℝ)*tailBudget x H T/B x -
      (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.m, OAI.TotientAsymptotic.tailBudget, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.gamma, OAI.TotientAsymptotic.alpha, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.maxD