OAI/NumberTheory/TwoPoint/Bounds/PrimeDefectMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact one-prime p² averages of the elementary modulus majorant.

  1. lemma OAI.TwoPointCorrelations.sum_zero_multiples_of_dvd line 13
  2. lemma OAI.TwoPointCorrelations.primeDefectLocal_sum line 26
  3. lemma OAI.TwoPointCorrelations.primeDefectLocal_average line 37