OAI/NumberTheory/CubicMoment/Estimates/HeckeLogDerivativeBand.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The absolute logarithmic-derivative bound on the inner half of a zero-free band. This is the estimate used when shifting prime-sum contours.

  1. theorem OAI.CubicFirstMoment.hecke_logDeriv_norm_of_zero_free_band line 11