OAI/NumberTheory/CubicMoment/Estimates/PrimeExclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit cost of the coprimality exclusion in a prime constituent. It follows from the proved ideal-divisor bound, uniformly in the excluded element, and will be subtracted from the prime Siegel–Walfisz estimate.

  1. lemma OAI.CubicFirstMoment.prime_exclusion_difference line 13
  2. theorem OAI.CubicFirstMoment.prime_exclusion_small_power line 31