OAI/NumberTheory/CubicMoment/Estimates/PrimeChebyshevDeweight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the logarithmic prime weight by Abel summation above sqrt X. The small primes are bounded by the actual Eisenstein lattice count.

  1. lemma OAI.CubicFirstMoment.primeCutoffSum_split line 15
  2. lemma OAI.CubicFirstMoment.inverseLogWeight_prime_cancel line 27
  3. lemma OAI.CubicFirstMoment.primeChebyshev_deweight line 36