OAI/NumberTheory/CubicMoment/Estimates/GrowthDischargedMains.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact main statements with the auxiliary Heath-Brown growth inputs removed. The required polynomial strip growth is derived from the original Voronoi identity.

  1. theorem OAI.CubicFirstMoment.mainResults_of_polynomial_inputs line 14
  2. theorem OAI.CubicFirstMoment.mainResults_of_hecke_voronoi_and_meanSquare line 57