OAI/NumberTheory/CubicMoment/Estimates/TailHighDecomposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact separation of the original prime Gauss tail into the two low-scale contributions, the remaining prime groups, and semiprimes.

  1. def OAI.CubicFirstMoment.tailHighOrdinaryArity line 15
  2. def OAI.CubicFirstMoment.tailHighUpperArity line 20
  3. lemma OAI.CubicFirstMoment.tailArity_height_scale_split line 25
  4. theorem OAI.CubicFirstMoment.primeProductGaussTail_scale_decomposition line 41