OAI/NumberTheory/CubicMoment/Estimates/PrimeReciprocal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The prime reciprocal estimate used in the smooth-number discard, derived from ordinary prime counting by literal Abel summation.

  1. lemma OAI.CubicFirstMoment.primaryPrimeMultiplicity_one line 13
  2. lemma OAI.CubicFirstMoment.inverse_square_continuous line 23
  3. lemma OAI.CubicFirstMoment.primaryPrime_reciprocal_integrable line 29
  4. lemma OAI.CubicFirstMoment.primaryPrime_reciprocal_identity line 41
  5. theorem OAI.CubicFirstMoment.primaryPrime_reciprocal_upper line 77