OAI/NumberTheory/CubicMoment/Estimates/HeckePrimeSquareDisk.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Sharp prime bounds from the actual square series and its proved disk bound. This accommodates finite Euler corrections in angular characters.

  1. theorem OAI.CubicFirstMoment.hecke_smooth_prime_bound_square_disk line 13
  2. theorem OAI.CubicFirstMoment.hecke_dyadic_prime_bound_of_square_disk line 68
  3. theorem OAI.CubicFirstMoment.hecke_full_prime_bound_of_square_disk line 143
  4. theorem OAI.CubicFirstMoment.hecke_prime_ideal_bound_of_square_disk line 181