OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstNoStopTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal ordinary-height no-stop row in the prime tail has the published Type-I saving. Its failed first-stage prefix is preserved.

  1. lemma OAI.CubicFirstMoment.scaleFirstTailNoStopRow_eq_window line 14
  2. theorem OAI.CubicFirstMoment.scaleFirstTailNoStopRow_finite_bound line 25