OAI/NumberTheory/TotientAsymptotic/RenewalTail.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tail coefficients in (1-F(z))/(1-z/rho).

  1. lemma OAI.TotientAsymptotic.a_le_a_succ line 11
  2. def OAI.TotientAsymptotic.renewalTail line 24
  3. lemma OAI.TotientAsymptotic.summable_renewalTail line 26
  4. lemma OAI.TotientAsymptotic.renewalTail_zero line 41
  5. lemma OAI.TotientAsymptotic.renewalTail_nonneg line 44
  6. lemma OAI.TotientAsymptotic.renewalTail_le_succ line 47
  7. lemma OAI.TotientAsymptotic.renewalTail_recurrence line 55
  8. lemma OAI.TotientAsymptotic.renewalTail_second_difference_neg line 71