OAI/NumberTheory/CubicMoment/Estimates/HeckeZeroFreeLog.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic zero-free width obtained from the actual polynomial Hecke disk bounds, for a character and its square.

  1. theorem OAI.CubicFirstMoment.hecke_zero_free_log_of_disks line 10
  2. theorem OAI.CubicFirstMoment.hecke_zero_free_log_from_analytic_pair line 41