OAI/NumberTheory/CubicMoment/Decomposition/PrimeProductPolynomialBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Height-independent bounds for the actual two full prime convolutions. These are used only beyond the power range of the published height mean.

  1. def OAI.CubicFirstMoment.primeCoefficientMassConstant line 15
  2. lemma OAI.CubicFirstMoment.fullPrimeCoefficient_l1_unit line 17
  3. def OAI.CubicFirstMoment.fullPrimeProductGauss line 36
  4. def OAI.CubicFirstMoment.fullPrimeProductModel line 43
  5. lemma OAI.CubicFirstMoment.fullPrimeProduct_centered line 51
  6. lemma OAI.CubicFirstMoment.fullPrimeProduct_weighted_bound line 67
  7. lemma OAI.CubicFirstMoment.fullPrimeProductGauss_bound line 93
  8. lemma OAI.CubicFirstMoment.fullPrimeProductModel_bound line 125
  9. lemma OAI.CubicFirstMoment.continuous_fullPrimeProductGauss line 190