OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstTailDecompositionRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact scale-first and two-stage stopping identities for the original Gauss height windows. Every matrix retains its total-product envelope.

  1. def OAI.CubicFirstMoment.scaleFirstTailScaleRow line 13
  2. lemma OAI.CubicFirstMoment.scaleFirstTail_arity_partition line 20
  3. theorem OAI.CubicFirstMoment.scaleFirstTailRoughWindow_by_scale line 35
  4. def OAI.CubicFirstMoment.scaleFirstTailNoStopRow line 68
  5. def OAI.CubicFirstMoment.scaleFirstTailStoppedRow line 80
  6. theorem OAI.CubicFirstMoment.scaleFirstTailScaleRow_two_stage line 90
  7. def OAI.CubicFirstMoment.scaleFirstTailStoppedDyad line 121
  8. theorem OAI.CubicFirstMoment.scaleFirstTailStoppedRow_dyads line 130