OAI/NumberTheory/CubicMoment/Decomposition/PrimeProductSharpMoments.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The prime-counting savings in the actual coefficients of an exceptional triple. These are consequences of the ordinary prime PNT; no moment estimate for the new paper is assumed.

  1. lemma OAI.CubicFirstMoment.fullPrimeSupport_subset_primeCutoff line 16
  2. lemma OAI.CubicFirstMoment.fullSquarefreePrimeSupport_card_le_product line 24
  3. theorem OAI.CubicFirstMoment.fullPrimeSupport_card_log_bound line 36
  4. theorem OAI.CubicFirstMoment.fullPrimeCoefficient_sharp_moments line 55
  5. theorem OAI.CubicFirstMoment.fullPrimeCoefficient_power_scale_moments line 101