OAI/NumberTheory/CubicMoment/Angular/AngularScaleFirstStoppedDyads.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact fixed-angular low-height stopping rows, retaining the original coefficients, product support, and inverse-binomial factors.

  1. def OAI.CubicFirstMoment.angular_distinguishedScaleStoppedRow line 12
  2. def OAI.CubicFirstMoment.angular_distinguishedScaleStopped line 30
  3. def OAI.CubicFirstMoment.angular_scaleFirstStoppedSum line 36
  4. def OAI.CubicFirstMoment.angular_distinguishedStoppedDyad line 40
  5. theorem OAI.CubicFirstMoment.angular_distinguishedScaleStoppedRow_dyads line 50