OAI/NumberTheory/CubicMoment/Estimates/ContinuationDischargedMains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact main statements after deriving continuation and all raw prime bounds. Continuation is built from the same Voronoi input; it is not an additional hypothesis.

  1. theorem OAI.CubicFirstMoment.mainResults_of_hecke_voronoi_and_heathBrown line 12