OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraSieveBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Numerical Bonferroni and CRT errors for the additional prime band. The truncation has order log(log N)/10, small enough for the true finite interval boundary and large enough for the actual small prime mass.

  1. lemma OAI.TwoPointCorrelations.mrt_extra_sieve_tail line 11
  2. lemma OAI.TwoPointCorrelations.mrt_extra_sieve_boundary line 26