RenewalLower.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform lower bounds for renewal coefficients and unbanded prefix coordinates.

lemma OAI.TotientAsymptotic.normalizedRenewal_pos line 14
lemma OAI.TotientAsymptotic.renewal_uniform_lower line 17
theorem OAI.TotientAsymptotic.unbanded_prefix_lower line 44
Source documentation
A terminal lower bound forces exponential growth towards the front of an unbanded prefix. The constant is independent of the dimension.
```
theorem unbanded_prefix_lower (hford : FordRenewalInput) :
    ∃ c : ℝ, 0 < c ∧ ∀ (N : ℕ) (u : ℕ → ℝ) (T : ℝ), 0 ≤ T → T ≤ u N →
      (∀ i < N, (∑ j ∈ Finset.Icc (i+1) N, a (j-i)*u j) ≤ u i) →
      ∀ i ≤ N, c*T*(rho^(N-i))⁻¹ ≤ u i := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.rho