OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraPrimeMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal mass in the additional large-prime interval. The exact logarithmic ratio and the small mass allow a short Bonferroni truncation.

  1. lemma OAI.TwoPointCorrelations.mrt_extra_prime_ratio line 12
  2. theorem OAI.TwoPointCorrelations.mrt_extra_prime_mass line 25