OAI/NumberTheory/CubicMoment/Estimates/LateStopDivisor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A late ordinary stop contains the required large smooth divisor. The divisor is the actual product of selected prime factors at or below the roughness boundary, not an auxiliary existence hypothesis.

  1. def OAI.CubicFirstMoment.lateStopDivisor line 14
  2. theorem OAI.CubicFirstMoment.stopped_late_smooth_divisor line 17