OAI/NumberTheory/TotientAsymptotic/RenewalConcavity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Concrete concavity of the coefficients in Ford's renewal recurrence.

  1. lemma OAI.TotientAsymptotic.a_shift_integral line 10
  2. lemma OAI.TotientAsymptotic.log_shift_intervalIntegrable line 17
  3. lemma OAI.TotientAsymptotic.log_second_difference_pos line 27
  4. lemma OAI.TotientAsymptotic.a_second_difference_neg line 37

    Source documentation

    The strict second difference used in Ford Lemma 3.7.

    lemma a_second_difference_neg {j : ℕ} (hj : 1≤j) :
    a (j+2)-2*a (j+1)+a j<0 := by
…

    Mentions: OAI.TotientAsymptotic.a