OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeTailMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mertens mass on power-logarithmic prime tails, uniformly in the exponent. This is the common finite prime range in both VK applications.

  1. def OAI.TwoPointCorrelations.mrtPrimePowerTail line 12
  2. theorem OAI.TwoPointCorrelations.mrt_prime_power_tail_mass line 15