OAI/NumberTheory/CubicMoment/Estimates/UpperTailGrouping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual upper-height prime boxes have a shorter group of size at least X^(1/3-3κ). The grouping uses one surviving tuple and fixed box scales.

  1. lemma OAI.CubicFirstMoment.tailPrimeTuple_upper_exponents line 14
  2. theorem OAI.CubicFirstMoment.eventually_tailPrimeTuple_upper_grouping line 53