OAI/NumberTheory/TotientAsymptotic/Renewal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Existence, uniqueness and positivity of the renewal parameters.

  1. lemma OAI.TotientAsymptotic.a_eq_integral line 13
  2. lemma OAI.TotientAsymptotic.a_pos line 19
  3. lemma OAI.TotientAsymptotic.a_le_log line 30
  4. lemma OAI.TotientAsymptotic.a_le_index line 39
  5. def OAI.TotientAsymptotic.renewalSeries line 43
  6. lemma OAI.TotientAsymptotic.summable_index_geometric line 45
  7. lemma OAI.TotientAsymptotic.summable_renewal line 53
  8. lemma OAI.TotientAsymptotic.renewalSeries_continuousOn line 60
  9. lemma OAI.TotientAsymptotic.renewalSeries_strictMonoOn line 72
  10. lemma OAI.TotientAsymptotic.renewalSeries_zero line 81
  11. lemma OAI.TotientAsymptotic.renewalSeries_nine_tenths_gt_one line 84
  12. theorem OAI.TotientAsymptotic.renewal_root_exists_unique line 92
  13. lemma OAI.TotientAsymptotic.rho_mem line 108
  14. lemma OAI.TotientAsymptotic.rho_pos line 115
  15. lemma OAI.TotientAsymptotic.rho_lt_one line 116
  16. lemma OAI.TotientAsymptotic.renewalSeries_rho line 117
  17. lemma OAI.TotientAsymptotic.lam_pos line 119
  18. lemma OAI.TotientAsymptotic.summable_moment line 123
  19. lemma OAI.TotientAsymptotic.gamma_pos line 134
  20. lemma OAI.TotientAsymptotic.alpha_pos line 142