OAI/NumberTheory/TwoPoint/ShortIntervals/MRTShortTheorem.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Corrected MRT Theorem 1.7 at every natural scale, reduced only to the sparse-prime and high-prime estimates used in the analytic argument.

  1. theorem OAI.TwoPointCorrelations.mrt_short_exponential_of_prime_estimates line 13