OAI/NumberTheory/CubicMoment/Decomposition/StoppedDyadRestriction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The original squarefree sharp dyad is exactly the full analytic stopped interval. Its possible norm-one term vanishes by the genuine stopping lower bound, rather than being discarded from the finite sum.

  1. lemma OAI.CubicFirstMoment.stoppedRowCoefficient_geometric_shift line 14
  2. lemma OAI.CubicFirstMoment.stoppedRowCoefficient_geometric_shift_of_bounds line 31
  3. theorem OAI.CubicFirstMoment.stoppedBeta_sharp_dyad_to_row line 47