OAI/NumberTheory/CubicMoment/Estimates/AnalyticDiskLowerBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The real lower bound obtained by retaining one zero in the local logarithmic-derivative expansion. All other zero terms have nonnegative real part on the zero-free right half-plane.

  1. lemma OAI.CubicFirstMoment.reciprocal_real_nonneg line 12
  2. theorem OAI.CubicFirstMoment.normalized_disk_logDeriv_real_lower_bound line 17
  3. theorem OAI.CubicFirstMoment.normalized_disk_logDeriv_lower_bound line 35