PrefixLower.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Propagating the first discrete tail coordinate through the prefix.

theorem OAI.TotientAsymptotic.renewal_prefix_lower line 14
Source documentation
The renewal recurrence propagates any terminal lower bound through the triangular prefix inequalities. This includes the first discrete tail prime.
```
theorem renewal_prefix_lower (N : ℕ) (u : ℕ → ℝ)
    (hs : ∀ i < N, (∑ j ∈ Finset.Icc (i+1) N, a (j-i)*u j) ≤ u i)
    {i : ℕ} (hi : i ≤ N) : g (N-i)*u N ≤ u i := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.g