OAI/NumberTheory/CubicMoment/Estimates/HeckeSquareDisk.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The existing zero-free argument needs only the actual square series and its normalized disk bound. This permits the proved finite Euler correction.

  1. theorem OAI.CubicFirstMoment.hecke_zero_free_log_from_square_disk line 11
  2. theorem OAI.CubicFirstMoment.hecke_logDeriv_norm_uniform_from_square_disk line 39