OAI/NumberTheory/TotientAsymptotic/RenewalSeriesAlgebra.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Formal coefficient identities for Ford's transformed recurrence.

  1. def OAI.TotientAsymptotic.Lseries line 11
  2. def OAI.TotientAsymptotic.Pseries line 12
  3. def OAI.TotientAsymptotic.Useries line 13
  4. def OAI.TotientAsymptotic.Aseries line 14
  5. def OAI.TotientAsymptotic.Gseries line 15
  6. def OAI.TotientAsymptotic.Hseries line 16
  7. lemma OAI.TotientAsymptotic.U_kernel_identity line 18
  8. lemma OAI.TotientAsymptotic.kernel_factorization line 31
  9. lemma OAI.TotientAsymptotic.L_H_identity line 51
  10. lemma OAI.TotientAsymptotic.L_A_identity line 57
  11. lemma OAI.TotientAsymptotic.G_A_identity line 74
  12. lemma OAI.TotientAsymptotic.G_H_identity line 89
  13. def OAI.TotientAsymptotic.renewalRegular line 97

    Source documentation

    The coefficients of the regular factor are uniformly bounded by four.

    def renewalRegular (n : ℕ) : ℝ := PowerSeries.coeff n Hseries

    Mentions: OAI.TotientAsymptotic.Hseries

  14. lemma OAI.TotientAsymptotic.renewalRegular_bound line 99
  15. lemma OAI.TotientAsymptotic.renewalRegular_zero line 122
  16. lemma OAI.TotientAsymptotic.renewalRegular_recurrence line 125
  17. lemma OAI.TotientAsymptotic.renewalTail_regular_convolution line 135