OAI/NumberTheory/CubicMoment/Estimates/HeckeFullPrimeEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full sharp ideal von Mangoldt bound, from the actual Hecke functional equations and the proved finite dyadic reconstruction.

  1. theorem OAI.CubicFirstMoment.hecke_full_prime_bound_of_analytic_pair line 11