OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstStoppedDyads.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact dyadic form of each original stopped row. The inverse binomial scalar and both stopping predicates are retained.

  1. def OAI.CubicFirstMoment.distinguishedStoppedAlpha line 13
  2. def OAI.CubicFirstMoment.distinguishedStoppedBeta line 18
  3. def OAI.CubicFirstMoment.distinguishedStoppedSide line 27
  4. def OAI.CubicFirstMoment.distinguishedStoppedDyad line 30
  5. theorem OAI.CubicFirstMoment.distinguishedScaleStoppedRow_dyads line 40