OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual integer-interval density of missing the additional prime band. Both sieve errors are paid, with no independence assumption on integers.

  1. theorem OAI.TwoPointCorrelations.mrt_extra_prime_avoidance line 12