OAI/NumberTheory/CubicMoment/Estimates/UpperTailStopping.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The upper-height branch uses one stopping threshold, X^(1/3-κ). The identity retains the actual envelope and inverse binomial weights.

  1. lemma OAI.CubicFirstMoment.eventually_distinguishedScale_upper_initial line 15
  2. def OAI.CubicFirstMoment.upperTailNoStopRow line 27
  3. def OAI.CubicFirstMoment.upperTailStoppedRow line 34
  4. theorem OAI.CubicFirstMoment.scaleFirstTailScaleRow_upper_stopping line 48
  5. theorem OAI.CubicFirstMoment.upperTailNoStopRow_finite_bound line 74