OAI/NumberTheory/CubicMoment/Estimates/TailPrimeSmallRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual small prime groups meet the localized length range. Constants from their fixed support widths are retained until a genuine exponent or logarithmic margin absorbs them.

  1. theorem OAI.CubicFirstMoment.eventually_tailPrime_small_localized_length line 12
  2. lemma OAI.CubicFirstMoment.tailPrime_low_upper_of_constant line 44
  3. theorem OAI.CubicFirstMoment.eventually_tailPrime_small_low_upper line 60
  4. theorem OAI.CubicFirstMoment.eventually_tailPrime_small_high_upper line 81