OAI/NumberTheory/CubicMoment/Estimates/PrimeTupleSize.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A polynomial bound for the actual von Mangoldt tuple sum. This coarse bound is used only against arbitrarily rapid Mellin tails.

  1. lemma OAI.CubicFirstMoment.vonMangoldt_coeff_norm_le line 14
  2. lemma OAI.CubicFirstMoment.vonMangoldt_tuple_core_bound line 23
  3. theorem OAI.CubicFirstMoment.vonMangoldt_unsplit_size line 52