OAI/NumberTheory/CubicMoment/Estimates/HeckeDiskLowerBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the fixed-disk logarithmic-derivative bound to the literal Hecke continuation, keeping the contribution of a nearby zero.

  1. lemma OAI.CubicFirstMoment.entire_zero_order_pos line 12
  2. theorem OAI.CubicFirstMoment.hecke_logDeriv_real_lower_of_disk line 23
  3. theorem OAI.CubicFirstMoment.hecke_logDeriv_lower_of_disk line 63