OAI/NumberTheory/CubicMoment/Decomposition/NoStopParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's actual no-stop threshold is short enough for Type I. All scale conditions are derived from their strict numerical exponent gaps.

  1. lemma OAI.CubicFirstMoment.eventually_noStop_scales line 12
  2. theorem OAI.CubicFirstMoment.noStop_patterson_isLittleO line 32