OAI/NumberTheory/CubicMoment/Estimates/SinglePrimeSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A prime convolution with one coordinate equals its weighted prime set, with the same exclusions and weights in the semiprime application.

  1. lemma OAI.CubicFirstMoment.orderedConvolutionSupport_unit line 12
  2. lemma OAI.CubicFirstMoment.orderedConvolution_unit line 24
  3. lemma OAI.CubicFirstMoment.fullSquarefreePrimeSupport_unit line 48
  4. lemma OAI.CubicFirstMoment.fullPrimeCoefficient_unit line 61