OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstStopping.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual low scale-first rows satisfy the two-stage stopping identity. The no-stop prefix test and both independent stopped matrices are retained exactly.

  1. def OAI.CubicFirstMoment.stoppingFailedPrefix line 16
  2. def OAI.CubicFirstMoment.distinguishedScaleStoppedRow line 21
  3. def OAI.CubicFirstMoment.distinguishedScaleStopped line 39
  4. theorem OAI.CubicFirstMoment.distinguishedScaleRow_two_stage line 45
  5. theorem OAI.CubicFirstMoment.distinguishedLowScaleRows_two_stage line 96