OAI/NumberTheory/CubicMoment/Estimates/SemiprimeHeightBlock.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The genuine semiprime Gauss polynomial has a uniform dyadic height mean throughout the range used to truncate its Mellin transform.

  1. def OAI.CubicFirstMoment.semiprimeGaussPolynomial line 13
  2. lemma OAI.CubicFirstMoment.semiprimeGaussPolynomial_symm line 21
  3. lemma OAI.CubicFirstMoment.semiprime_height_power line 32
  4. theorem OAI.CubicFirstMoment.semiprime_gauss_height_log_saving line 40