OAI/NumberTheory/TotientAsymptotic/RenewalConvolution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The dominated convolution limit needed for the finite-tail volume asymptotic. The sole published input here is Ford's bounded renewal error, Lemma 3.7 of The distribution of totients, arXiv:1104.3264v2 (2013), with Ford's constant lambda denoted by gamma in this development.

  1. def OAI.TotientAsymptotic.FordRenewalInput line 18
  2. def OAI.TotientAsymptotic.normalizedRenewal line 21
  3. lemma OAI.TotientAsymptotic.normalizedRenewal_properties line 23
  4. def OAI.TotientAsymptotic.renewalConvolution line 46
  5. lemma OAI.TotientAsymptotic.renewalConvolution_eq_tsum line 49
  6. theorem OAI.TotientAsymptotic.renewalConvolution_tendsto line 62

    Source documentation

    Summable arithmetic tail weights can be passed through the normalized renewal convolution without requiring any continuity in the phase.

    theorem renewalConvolution_tendsto (hford : FordRenewalInput)
    (c : ℕ → ℝ) (hc : Summable c) :
    Tendsto (renewalConvolution c) atTop (nhds (gamma * ∑' i, c i)) := by
…

    Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.renewalConvolution, OAI.TotientAsymptotic.gamma