OAI/NumberTheory/CubicMoment/Estimates/UpperStoppedRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The upper one-stage stopping range fits the high-height bilinear estimate once κ is chosen inside its published power-width margin.

  1. theorem OAI.CubicFirstMoment.eventually_upper_stopped_analytic_range line 11