OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterPrimeTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform absolute bound for the prime tail at sigma=1+1/log X. The proof groups primes into intervals whose logarithms have width log X and applies Mertens' first theorem in each interval.

  1. lemma OAI.TwoPointCorrelations.mrt_finite_exp_sum line 14
  2. theorem OAI.TwoPointCorrelations.mrt_character_prime_tail_bound line 36