OAI/NumberTheory/CubicMoment/Angular/AngularTailHighDecomposition.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.angular_tailHighOrdinaryArity line 16
  2. def OAI.CubicFirstMoment.angular_tailHighUpperArity line 21
  3. lemma OAI.CubicFirstMoment.angular_tailArity_height_scale_split line 26
  4. theorem OAI.CubicFirstMoment.angular_primeProductGaussTail_scale_decomposition line 42