OAI/NumberTheory/CubicMoment/Estimates/TailPrimeOrdinaryBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ordinary-height prefix on an actual group. Small groups use the logarithmic localization bound on two aligned full tails. Larger groups use the published Hecke estimate on each retained window.

  1. theorem OAI.CubicFirstMoment.tailPrime_ordinary_group_prefix line 19