OAI/NumberTheory/CubicMoment/Estimates/HeckeUniformGrowth.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A conductor-explicit polynomial bound in the fixed strip needed by the local zero-free argument. The finite-order constant disappears under Phragmen--Lindelof; only the actual functional-equation factors remain.

  1. def OAI.CubicFirstMoment.heckeZeroFreeMajorant line 14
  2. lemma OAI.CubicFirstMoment.heckeZeroFreeMajorant_ge_zeta line 17
  3. lemma OAI.CubicFirstMoment.heckeZeroFreeMajorant_pos line 24
  4. theorem OAI.CubicFirstMoment.shifted_hecke_uniform_strip line 28