OAI/NumberTheory/CubicMoment/Estimates/HeckeZeros.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Zeros of the actual entire Hecke continuations: none occur right of one, bounded sets contain finitely many, and local multiplicities are positive finite integers.

  1. theorem OAI.CubicFirstMoment.heckeSeries_ne_zero line 14
  2. theorem OAI.CubicFirstMoment.heckeZero_real_le_one line 22
  3. lemma OAI.CubicFirstMoment.entire_zeros_finite_on_compact line 30
  4. lemma OAI.CubicFirstMoment.entire_zero_local_factor line 41