OAI/NumberTheory/Ostmann/ZeroDensity/DigammaTailEstimate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded tail in the sharp positive-strip digamma comparison

  1. def OAI.Ostmann.densityDigammaTerm line 12
  2. theorem OAI.Ostmann.density_digamma_hasSum line 15
  3. theorem OAI.Ostmann.density_digamma_tail_bound line 22