OAI/NumberTheory/CubicMoment/Estimates/HeckePrimeControlled.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A quantitative smooth prime estimate with its explicit finite weight cost deduced from the actual Hecke functional equations for a character and its square. No prime bound or zero-free assertion is assumed.

  1. theorem OAI.CubicFirstMoment.hecke_smooth_prime_bound_controlled line 14