OAI/NumberTheory/CubicMoment/Estimates/LogarithmicPrimeWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The radial derivative bounds of a logarithmic family, used to apply the published prime Siegel–Walfisz input by actual partial summation.

  1. lemma OAI.CubicFirstMoment.LogarithmicWeightFamily.norm_log_bound line 12
  2. lemma OAI.CubicFirstMoment.LogarithmicWeightFamily.radial_deriv_bound line 27