OAI/NumberTheory/CubicMoment/Estimates/UpperNoStopParameters.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal no-stop thresholds in the two height ranges. The upper range uses the smaller stopping level required by the Type-I exponent.

  1. def OAI.CubicFirstMoment.heightNoStopThreshold line 12
  2. def OAI.CubicFirstMoment.heightNoStopOuterBound line 15
  3. lemma OAI.CubicFirstMoment.eventually_ordinary_noStop_window_scales line 18
  4. lemma OAI.CubicFirstMoment.eventually_upper_noStop_window_scales line 36
  5. lemma OAI.CubicFirstMoment.eventually_height_noStop_window_scales line 54