OAI/NumberTheory/CubicMoment/Estimates/TailPrimeMiddleRange.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual intermediate prime-group range meets both length and height hypotheses of the enlarged dispersion estimate, with fixed support widths retained.

  1. theorem OAI.CubicFirstMoment.eventually_tailPrime_middle_upper line 12
  2. theorem OAI.CubicFirstMoment.eventually_tailPrime_middle_height line 36