OAI/NumberTheory/CubicMoment/Estimates/LongPrimeLogScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The long-prime threshold gives the actual logarithmic parameter range required by the published prime estimate, even after bin dilation.

  1. theorem OAI.CubicFirstMoment.long_prime_logarithmic_window line 11